summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Arith')
-rw-r--r--backends/lean/Base/Arith/Base.lean6
1 files changed, 6 insertions, 0 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index a6e59b74..e008f7b9 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -28,6 +28,12 @@ theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by
| .inl _ => left; linarith
| .inr _ => right; linarith
+-- TODO: move?
+theorem add_one_le_iff_le_ne (n m : Nat) (h1 : m ≤ n) (h2 : m ≠ n) : m + 1 ≤ n := by
+ -- Damn, those proofs on natural numbers are hard - I wish Omega was in mathlib4...
+ simp [Nat.add_one_le_iff]
+ simp [Nat.lt_iff_le_and_ne]
+ simp_all
/- Induction over positive integers -/
-- TODO: move