X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2Fnat.ma;h=f15f8cbc858becfb524e6259b644cf6a7b841230;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=4f1f6541164044c5b6be1e3a4117f4f73988b498;hpb=0a5e353bdadc4194e8becc7b960088ed4dbf68c1;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 4f1f65411..f15f8cbc8 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -80,10 +80,6 @@ napply nat_elim2; #n;
  ##[ ncases n; /2/;
  ##| /3/;
  ##| #m; #Hind; ncases Hind;/3/;
- (* 
- ##[/2/; ##|#H; nwhd; 
-    napply or_introl;
-    napply eq_f2; /3/; *)
  ##]
 nqed. 
 
@@ -127,7 +123,7 @@ ntheorem associative_plus : associative nat plus.
 #n; nelim n; nnormalize; //; nqed.
 
 ntheorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
-//; nqed.
+//; nqed. 
 
 ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 #n; nelim n; nnormalize; /3/; nqed.
@@ -261,6 +257,9 @@ ntheorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
 ntheorem le_O_n : ∀n:nat. O ≤ n.
 #n; nelim n; /2/; nqed.
 
+ntheorem nboh: 0 ≤ 0 + 0.
+//; nqed.
+
 ntheorem le_n_Sn : ∀n:nat. n ≤ S n.
 /2/; nqed.
 
@@ -276,8 +275,6 @@ ntheorem monotonic_pred: monotonic ? le pred.
 #n; #m; #lenm; nelim lenm; /2/;nqed.
 
 ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
-(* XXX *) nletin hint ≝ monotonic. 
-#a; #b; #H; napplyS monotonic_pred;
 /2/; nqed.
 
 (* this are instances of the le versions 
@@ -453,9 +450,8 @@ ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
 (* le and eq *)
 
 ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-napply nat_elim2; 
-##[#n; #H1; #H2; /4/;
- nqed. 
+napply nat_elim2; /4/;
+nqed. 
 
 ntheorem lt_O_S : ∀n:nat. O < S n.
 /2/; nqed.