propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_le_plus.ma

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 d54738f250b4100fea5bbdde0c20518572aad361..7a53e23f745851ddc67afeab505582aa40f4592e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
@@ -39,7 +39,11 @@ lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m.
 /2 width=1 by nle_plus_bi_sn/ qed.
 
 (*** le_plus_a *)
-lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
+lemma nle_plus_dx_sn (o) (m) (n): n ≤ m → n ≤ o + m.
+/2 width=3 by nle_trans/ qed.
+
+(*** le_plus_b *)
+lemma nle_plus_dx_dx (o) (m) (n): n ≤ m → n ≤ m + o.
 /2 width=3 by nle_trans/ qed.
 
 (* Main constructions with nplus ********************************************)