theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n).
/2/ qed.
-theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
-/2/ qed.
-
theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
// qed.
(* Negated equalities *******************************************************)
+theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+/2/ qed.
+
theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
#n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
#a #b #c #H @(le_plus_to_le_r … b) /2/
qed.
+lemma lt_to_le: ∀x,y. x < y → x ≤ y.
+/2 width=2/ qed.
+
+lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
+// qed-.
+
+lemma le_x_times_x: ∀x. x ≤ x * x.
+#x elim x -x //
+qed.
+
(* lt *)
theorem transitive_lt: transitive nat lt.
]
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
+cut (∀n,a. f a = n → P a) /2 width=3/ -a
+#n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto very slow (274s) without #n *)
+qed-.
+
(* More negated equalities **************************************************)
theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
#x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
*)
+lemma minus_le: ∀x,y. x - y ≤ x.
+/2 width=1/ qed.
+
(* lt *)
theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
@lt_plus_to_minus_r <plus_minus_m_m //
qed.
+(* More compound conclusion *************************************************)
+
+lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+* /2 width=1/ #x * /2 width=1/ #y normalize #H
+lapply (minus_le x y) <H -H #H
+elim (not_le_Sn_n x) #H0 elim (H0 ?) //
+qed-.
+
(* Still more equalities ****************************************************)
theorem eq_minus_O: ∀n,m:nat.
lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
/2 width=1/ qed.
+lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
+// qed.
+
(* Stilll more atomic conclusion ********************************************)
(* le *)
lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
#i #n #m #leni #lemi normalize (cases (leb n m))
normalize // qed.
-