X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_lt.ma;h=1df0f857d54d9edc95a70ec09e9cee1e2ddd5298;hp=fc445dd74a36dbcbdb02ffb0f610e2c43af66f50;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hpb=df7a2aa19e98dc28e7f22129275a175cead49e2d

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
index fc445dd74..1df0f857d 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
@@ -26,6 +26,12 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
+lemma nlt_i (m) (n): ↑m ≤ n → m < n.
+// qed.
+
+lemma nlt_refl_succ (n): n < ↑n.
+// qed.
+
 (*** lt_O_S *)
 lemma nlt_zero_succ (m): 𝟎 < ↑m.
 /2 width=1 by nle_succ_bi/ qed.