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

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index cc6b19deb..649108f47 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -242,7 +242,7 @@ theorem monotonic_le_plus_l:
 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2 
 → n1 + m1 ≤ n2 + m2.
 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
-/2/ qed-.
+/2/ qed.
 
 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
 /2/ qed. 
@@ -595,8 +595,10 @@ theorem increasing_to_le: ∀f:nat → nat.
 @(ex_intro ?? (S a)) /2/
 qed.
 
+(* thus is le_plus
 lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
-/3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
+#x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
+*)
 
 (* lt *)