X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_le_plus.ma;h=bbca72f279d9499fd8cf33d4c48f5532acb8c7f1;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hp=513ea525701c2ca2e2c24e219c73ec0854acf202;hpb=df7a2aa19e98dc28e7f22129275a175cead49e2d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
index 513ea5257..bbca72f27 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
@@ -15,9 +15,9 @@
 include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_le.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************)
 
-(* Basic constructions with plus ********************************************)
+(* Constructions with nplus ***********************************************************)
 
 (*** monotonic_le_plus_l *)
 lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
@@ -46,14 +46,14 @@ lemma nle_plus_dx_dx (m) (n) (o): n + o ≤ m → n ≤ m.
 lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
 /2 width=3 by nle_trans/ qed.
 
-(* Main constructions with plus *********************************************)
+(* Main constructions with nplus ********************************************)
 
 (*** le_plus *)
 theorem nle_plus_bi (m1) (m2) (n1) (n2):
         m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
 /3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.
 
-(* Basic inversions with plus ***********************************************)
+(* Inversions with nplus ****************************************************)
 
 (*** plus_le_0 *)
 lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
@@ -61,10 +61,9 @@ lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
 
 (*** le_plus_to_le_r *)
 lemma nle_inv_plus_bi_dx (o) (m) (n): n + o ≤ m + o → n ≤ m.
-#o @(nat_ind … o) -o /3 width=1 by nle_inv_succ_bi/
+#o @(nat_ind_succ … o) -o /3 width=1 by nle_inv_succ_bi/
 qed-.
 
 (*** le_plus_to_le *)
 lemma nle_inv_plus_bi_sn (o) (m) (n): o + n ≤ o + m → n ≤ m.
 /2 width=2 by nle_inv_plus_bi_dx/ qed-.
-