X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_lt_plus.ma;h=0f0a21c829a551516ca199498b200384e5c32eab;hp=89af3af2b449a9945de8419dab10d8befd8f7b56;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hpb=77c9255de3c5f7780aeacd745703a1cc76328a68

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma
index 89af3af2b..0f0a21c82 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma
@@ -31,6 +31,12 @@ lemma nlt_plus_bi_sn (m) (n1) (n2): n1 < n2 → m + n1 < m + n2.
 @nlt_i >nplus_succ_dx /2 width=1 by nle_plus_bi_sn/
 qed.
 
+lemma nlt_plus_dx_dx (o) (m) (n): m < n → m < n + o.
+/2 width=1 by nle_plus_dx_dx/ qed.
+
+lemma nlt_plus_dx_sn (o) (m) (n) : m < n → m < o + n.
+/2 width=1 by nle_plus_dx_sn/ qed.
+
 lemma nlt_succ_plus_dx_refl_sn (m) (n): m < ↑(m + n).
 /2 width=1/ qed.