feat(data/nat/basic): decreasing induction (#1031)

* feat(data/nat/basic): decreasing induction

* feat(data/nat/basic): better proof of decreasing induction

Author: sgouezel

src/data/nat/basic.lean

@@ -27,7 +27,7 @@ theorem succ_inj' {n m : ℕ} : succ n = succ m ↔ n = m :=
 theorem succ_le_succ_iff {m n : ℕ} : succ m ≤ succ n ↔ m ≤ n :=
 ⟨le_of_succ_le_succ, succ_le_succ⟩
 
-lemma zero_max {m : nat} : max 0 m = m := 
+lemma zero_max {m : nat} : max 0 m = m :=
 max_eq_right (zero_le _)
 
 theorem max_succ_succ {m n : ℕ} :
@@ -45,7 +45,7 @@ succ_le_succ_iff
 lemma succ_le_iff {m n : ℕ} : succ m ≤ n ↔ m < n :=
 ⟨lt_of_succ_le, succ_le_of_lt⟩
 
-lemma lt_iff_add_one_le {m n : ℕ} : m < n ↔ m + 1 ≤ n := 
+lemma lt_iff_add_one_le {m n : ℕ} : m < n ↔ m + 1 ≤ n :=
 by rw succ_le_iff
 
 theorem of_le_succ {n m : ℕ} (H : n ≤ m.succ) : n ≤ m ∨ n = m.succ :=
@@ -1061,4 +1061,9 @@ lemma with_bot.add_eq_one_iff : ∀ {n m : with_bot ℕ}, n + m = 1 ↔ (n = 0 
   ∀ n ≥ m, P n :=
 by apply nat.less_than_or_equal.rec h0; exact h1
 
+@[elab_as_eliminator]
+lemma decreasing_induction {P : ℕ → Prop} (h : ∀n, P (n+1) → P n) {m n : ℕ} (nm : m ≤ n) (hP : P n) :
+  P m :=
+by { induction nm with n nm ih, exact hP, exact ih (h _ hP) }
+
 end nat