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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
index fc445dd74..388c8aace 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
@@ -14,7 +14,7 @@
 
 include "ground/arith/nat_le.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
 
 (*** lt *)
 definition nlt: relation2 nat nat ≝
@@ -26,10 +26,19 @@ 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.
 
+lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n.
+/2 width=1 by nle_succ_bi/ qed.
+
 (*** le_to_or_lt_eq *)
 lemma nle_lt_eq_e (m) (n): m ≤ n → ∨∨ m < n | m = n.
 #m #n * -n /3 width=1 by nle_succ_bi, or_introl/