feat(library/data/nat/wf): predecessor relation is well-founded

library/data/nat/wf.lean

@@ -4,9 +4,36 @@
 import data.nat.order logic.wf
 open nat eq.ops
 
+namespace nat
+
+inductive pred_rel : nat → nat → Prop :=
+intro : Π (n : nat), pred_rel n (succ n)
+
+definition not_pred_rel_zero (n : nat) : ¬ pred_rel n zero :=
+have aux : ∀{m}, pred_rel n m → succ n = m, from
+  λm H, pred_rel.rec_on H (take n, rfl),
+assume H : pred_rel n zero,
+  absurd (aux H) !succ_ne_zero
+
+definition pred_rel_succ {a b : nat} (H : pred_rel a (succ b)) : b = a :=
+have aux : pred (succ b) = a, from
+  pred_rel.rec_on H (λn, rfl),
+aux
+
+-- Predecessor relation is well-founded
+definition pred_rel.wf : well_founded pred_rel :=
+well_founded.intro
+  (λn, induction_on n
+    (acc.intro zero (λy (H : pred_rel y zero), absurd H (not_pred_rel_zero y)))
+    (λa (iH : acc pred_rel a),
+       acc.intro (succ a) (λy (H : pred_rel y (succ a)),
+         have aux : a = y, from pred_rel_succ H,
+         eq.rec_on aux iH)))
+
+-- Less-than relation is well-founded
 definition lt.wf [instance] : well_founded lt :=
 well_founded.intro
- (take n, nat.induction_on n
+ (λn, induction_on n
     (acc.intro zero (λ (y : nat) (H : y < 0),
       absurd H !not_lt_zero))
     (λ (n : nat) (iH : acc lt n),
@@ -15,3 +42,5 @@ well_founded.intro
         or.elim H₁
           (assume Hlt : m < n, acc.inv iH Hlt)
           (assume Heq : m = n, Heq⁻¹ ▸ iH))))
+
+end nat