X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_le_plus.ma;h=d54738f250b4100fea5bbdde0c20518572aad361;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=c1dd32661bb90ae09af5e7733b0c3488ac0a0429;hpb=19b0a814861157ba05f23877d5cd94059f52c2e8;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 c1dd32661..d54738f25 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".
 
-(* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
 
-(* Constructions with nplus ***********************************************************)
+(* Constructions with nplus *************************************************)
 
 (*** monotonic_le_plus_l *)
 lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
@@ -38,10 +38,6 @@ lemma nle_plus_dx_dx_refl (m) (n): m ≤ m + n.
 lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m.
 /2 width=1 by nle_plus_bi_sn/ qed.
 
-(*** le_plus_b *)
-lemma nle_plus_dx_dx (m) (n) (o): n + o ≤ m → n ≤ m.
-/2 width=3 by nle_trans/ qed.
-
 (*** le_plus_a *)
 lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
 /2 width=3 by nle_trans/ qed.
@@ -55,6 +51,10 @@ theorem nle_plus_bi (m1) (m2) (n1) (n2):
 
 (* Inversions with nplus ****************************************************)
 
+(*** le_plus_b *)
+lemma nle_inv_plus_sn_dx (m) (n) (o): n + o ≤ m → n ≤ m.
+/2 width=3 by nle_trans/ qed.
+
 (*** plus_le_0 *)
 lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
 /3 width=1 by nle_inv_zero_dx, eq_inv_zero_nplus/ qed-.