(no commit message)

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 6f57893a5ac62d7c88039bf7c913bc3b684d8296..120a0bb16199c888d16866c495c1fbc7a2f1579e 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -112,7 +112,7 @@ ntheorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
 #n; nelim n; nnormalize; //; nqed.
 *)
 
-(*
+(* deleterio 
 ntheorem plus_n_SO : ∀n:nat. S n = n+S O.
 //; nqed. *)
 
@@ -293,9 +293,11 @@ ntheorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
 ntheorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
 /3/; nqed.
 
+naxiom decidable_le: ∀n,m. decidable (n≤m).
+(*
 ntheorem decidable_le: ∀n,m. decidable (n≤m).
 napply nat_elim2; #n; /3/;
-#m; #dec; ncases dec;/4/; nqed.
+#m; #dec; ncases dec;/4/; nqed. *)
 
 ntheorem decidable_lt: ∀n,m. decidable (n < m).
 #n; #m; napply decidable_le ; nqed.
@@ -558,7 +560,7 @@ ntheorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 
 ntheorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  \to m1 ≤ m2 
 → n1 + m1 ≤ n2 + m2.
-#n1; #n2; #m1; #m2; #len; #lem; napply transitive_le;
+#n1; #n2; #m1; #m2; #len; #lem; napply (transitive_le ? (n1+m2));
 /2/; nqed.
 
 ntheorem le_plus_n :∀n,m:nat. m ≤ n + m.
@@ -639,7 +641,7 @@ napply transitive_le; (* /2/ slow *)
 nqed.
 
 ntheorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
-(* bello *)
+#n; #m; #H; napplyS monotonic_le_times_l;
 /2/; nqed.
 
 ntheorem le_times_to_le: 
@@ -655,9 +657,9 @@ ntheorem le_times_to_le:
   ##]
 nqed.
 
-ntheorem le_S_times_2: ∀n,m.O < m → n ≤ m → n < 2*m.
+ntheorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
 #n; #m; #posm; #lenm; (* interessante *)
-nnormalize; napplyS (le_plus n); //; nqed.
+napplyS (le_plus n); //; nqed.
 
 (* times & lt *)
 (*