X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=cca4782806c2264ce0bc294a84bee55881d4a18c;hb=cd2f5b59215ea771ac137b9a7b115a05175f45d5;hp=56935028f65015812b79fdc15fb8762b012d14cf;hpb=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 56935028f..cca478280 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -164,7 +164,7 @@ lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 // 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.
@@ -187,6 +187,13 @@ theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
 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.
@@ -439,6 +446,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)
@@ -464,6 +475,11 @@ lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
 #m #n elim (decidable_le m n) /2/ /4/
 qed-.
 
+lemma le_inv_S1: ∀x,y. S x ≤ y → ∃∃z. x ≤ z & y = S z.
+#x #y #H elim H -y /2 width=3 by ex2_intro/
+#y #_ * #n #Hxn #H destruct /3 width=3 by le_S, ex2_intro/
+qed-. 
+
 (* More general conclusion **************************************************)
 
 theorem nat_ind_plus: ∀R:predicate nat.
@@ -495,6 +511,44 @@ 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-. 
+
+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.
@@ -560,7 +614,7 @@ pred n - pred m = n - m.
 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
 qed.
 
-theorem plus_minus_commutative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
+theorem plus_minus_associative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
 /2 by plus_minus/ qed.
 
 (* More atomic conclusion ***************************************************)
@@ -657,6 +711,10 @@ 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.
@@ -690,6 +748,9 @@ theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
 <commutative_plus <plus_minus_m_m //
 qed.
 
+lemma minus_minus_associative: ∀x,y,z. z ≤ y → y ≤ x → x - (y - z) = x - y + z.
+/2 width=1 by minus_minus/ qed-.
+
 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
 /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
 
@@ -703,6 +764,12 @@ lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
 lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
 // qed.
 
+lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
+// qed.
+
+lemma minus_plus_minus_l: ∀x,y,z. y ≤ z → (z + x) - (z - y) = x + y.
+/2 width=1 by minus_minus_associative/ qed-.
+
 (* Stilll more atomic conclusion ********************************************)
 
 (* le *)