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.
// qed.
theorem times_n_1 : ∀n:nat. n = n * 1.
-#n // qed.
+// qed.
theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
// qed.
lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
// qed.
+lemma discr_plus_xy_minus_xz: ∀x,z,y. x + y = x - z → y = 0.
+#x elim x -x // #x #IHx * normalize
+[ #y #H @(IHx 0) <minus_n_O /2 width=1/
+| #z #y >plus_n_Sm #H lapply (IHx … H) -x -z #H destruct
+]
+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.
theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
#n #m #lenm (elim lenm) /3/ qed.
+theorem eq_or_gt: ∀n. 0 = n ∨ 0 < n.
+#n elim (le_to_or_lt_eq 0 n ?) // /2 width=1/
+qed-.
+
theorem increasing_to_le2: ∀f:nat → nat. increasing f →
∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
#f #incr #m #lem (elim lem)
]
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.
#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-.
+
+lemma plus_le_0: ∀x,y. x + y ≤ 0 → x = 0 ∧ y = 0.
+#x #y #H elim (le_inv_plus_l … H) -H #H1 #H2 /3 width=1/
+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.
-