X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=cc6b19debaf147377cf02e9bfb39c26eea1201a5;hb=bdc0a7a8c1de693a40f116742f5d2d3f3290c381;hp=31d5ced7f7c64ac7dfa03ee8b6f96c65ad12a09b;hpb=84713c9446ff13dd26533590985a0df67cb5ec7e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 31d5ced7f..cc6b19deb 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -402,14 +402,14 @@ theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
 @nat_elim2 #n
  [#abs @False_ind /2/
  |/2/
- |#m #Hind #HnotleSS @le_S_S /3/
+ |#m #Hind #HnotleSS @le_S_S @Hind /2/ 
  ]
 qed.
 
 (* not lt, le *)
 
 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
-/4/ qed.
+#n #m #H @le_S_S_to_le @not_le_to_lt /2/ qed.
 
 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
@@ -441,17 +441,25 @@ theorem increasing_to_le2: ∀f:nat → nat. increasing f →
 qed.
 
 lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
-/3 width=2/ qed-.
+/3/ qed-.
 
 lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
-/3 width=2/ qed-.
+/3/ qed-.
 
 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
-#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
+#m #n elim (decidable_lt m n) /2/ /3/
+qed-.
+
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (decidable_le m n) /2/ /4/
 qed-.
 
 (* More general conclusion **************************************************)
 
+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
@@ -488,7 +496,7 @@ 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/
+@nat_elim2 /4 by le_n_O_to_eq, monotonic_pred, eq_f, sym_eq/
 qed. 
 
 theorem increasing_to_injective: ∀f:nat → nat.
@@ -594,7 +602,7 @@ lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 
 
 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
-#Heq /3/ qed-.
+#Heq @not_le_to_lt /2/ qed-.
 
 theorem lt_times_n_to_lt_l: 
 ∀n,p,q:nat. p*n < q*n → p < q.
@@ -636,7 +644,7 @@ qed.
 theorem distributive_times_minus: distributive ? times minus.
 #a #b #c
 (cases (decidable_lt b c)) #Hbc
- [> eq_minus_O /2/ >eq_minus_O // 
+ [> eq_minus_O [2:/2/] >eq_minus_O // 
   @monotonic_le_times_r /2/
  |@sym_eq (applyS plus_to_minus) <distributive_times_plus 
   @eq_f (applyS plus_minus_m_m) /2/
@@ -666,6 +674,9 @@ lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 #b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
 qed.
 
+lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
+/2 width=1/ qed.
+
 (* Stilll more atomic conclusion ********************************************)
 
 (* le *)
@@ -783,3 +794,4 @@ 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.
+