arithmetics for λδ

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
index f7a868b534a17de122ff7aa4f6a4f4b49a667bcd..388c8aace268d6a2e7d8c7658d618ff0918ce091 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
@@ -36,6 +36,9 @@ lemma nlt_refl_succ (n): n < ↑n.
 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/