le_induction

leanprover-community · Jan 23, 2019 · 6da9b21 · 6da9b21
1 parent 60efaec
commit 6da9b21
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
@@ -859,5 +859,10 @@ lemma with_bot.add_eq_one_iff : ∀ {n m : with_bot ℕ}, n + m = 1 ↔ (n = 0
 | (some n) (some (m + 1)) := by erw [with_bot.coe_eq_coe, with_bot.coe_eq_coe, with_bot.coe_eq_coe,
     with_bot.coe_eq_coe, with_bot.coe_eq_coe]; simp [nat.add_succ, nat.succ_inj', nat.succ_ne_zero]
 
+-- induction
+
+@[elab_as_eliminator] lemma le_induction {P : nat → Prop} {m} (h0 : P m) (h1 : ∀ n ≥ m, P n → P (n + 1)) : 
+  ∀ n ≥ m, P n :=
+by apply nat.less_than_or_equal.rec h0; exact h1
 
 end nat