+theorem nat_ind_plus: ∀R:predicate nat.
+ R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
+/3 by nat_ind/ qed-.
+
+theorem lt_O_n_elim: ∀n:nat. 0 < n →
+ ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
+#n (elim n) // #abs @False_ind /2/ @absurd
+qed.
+
+theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
+#n (cases n) // #a #abs @False_ind /2/ qed.
+
+theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
+∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
+#n #m #Hle #P (elim Hle) /3/ qed.
+
+theorem nat_elim1 : ∀n:nat.∀P:nat → Prop.
+(∀m.(∀p. p < m → P p) → P m) → P n.
+#n #P #H
+cut (∀q:nat. q ≤ n → P q) /2/
+(elim n)
+ [#q #HleO (* applica male *)
+ @(le_n_O_elim ? HleO)
+ @H #p #ltpO @False_ind /2/ (* 3 *)
+ |#p #Hind #q #HleS
+ @H #a #lta @Hind @le_S_S_to_le /2/
+ ]
+qed.
+
+fact f_ind_aux: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+ (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) →
+ ∀n,a. f a = n → P a.
+#A #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+ (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
+#A #f #P #H #a
+@(f_ind_aux … H) -H [2: // | skip ]
+qed-.
+
+fact f2_ind_aux: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
+ (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
+ ∀n,a1,a2. f a1 a2 = n → P a1 a2.
+#A1 #A2 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f2_ind: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
+ (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
+ ∀a1,a2. P a1 a2.
+#A1 #A2 #f #P #H #a1 #a2
+@(f2_ind_aux … H) -H [2: // | skip ]
+qed-.
+
+fact f3_ind_aux: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
+ (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
+ ∀n,a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3.
+#A1 #A2 #A3 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f3_ind: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
+ (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
+ ∀a1,a2,a3. P a1 a2 a3.
+#A1 #A2 #A3 #f #P #H #a1 #a2 #a3
+@(f3_ind_aux … H) -H [2: // | skip ]
+qed-.
+
+(* More negated equalities **************************************************)
+
+theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
+#n #m #H @not_to_not /2/ qed.
+
+(* More equalities **********************************************************)
+
+theorem le_n_O_to_eq : ∀n:nat. n ≤ 0 → 0=n.
+#n (cases n) // #a #abs @False_ind /2/ qed.
+
+theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
+@nat_elim2 /4 by le_n_O_to_eq, monotonic_pred, eq_f, sym_eq/
+qed.
+
+theorem increasing_to_injective: ∀f:nat → nat.
+ increasing f → injective nat nat f.
+#f #incr #n #m cases(decidable_le n m)
+ [#lenm cases(le_to_or_lt_eq … lenm) //
+ #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq
+ @increasing_to_monotonic //
+ |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq
+ @lt_to_not_eq @increasing_to_monotonic /2/
+ ]
+qed.