X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=7bd51c318fb99f02d2e158395fbd6f56ec7c0a9d;hb=520d4370a540a98f5e5e1d85acfef0c982cc1e04;hp=649108f47c27110a30a770489ce0d9f82bd221d3;hpb=7163f2ff5eb4960162d2fcf135f031ae2a9f8b56;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 649108f47..7bd51c318 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -135,9 +135,6 @@ theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 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.
 
@@ -192,6 +189,9 @@ lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
 
 (* 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.
 
@@ -299,6 +299,16 @@ theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
 #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.
@@ -429,6 +439,10 @@ theorem decidable_lt: ∀n,m. decidable (n < m).
 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)
@@ -485,6 +499,31 @@ cut (∀q:nat. q ≤ n → P q) /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-. 
+
 (* More negated equalities **************************************************)
 
 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
@@ -600,6 +639,9 @@ lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 
 #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.
@@ -636,6 +678,18 @@ theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
 @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.
@@ -679,6 +733,9 @@ qed.
 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 *)
@@ -796,4 +853,3 @@ lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
 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.
-