milestone update in ground, partial commit

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
index cb776975830572cff409fe9e0317ef6d852ce584..e05ff9473f0c36213c42ded225f6108a4defff77 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
@@ -38,10 +38,15 @@ lemma nlt_inv_succ_sn (m) (n): ↑m < n → ∧∧ m < ↓n & n = ↑↓n.
 lemma nlt_inv_pred_dx (m) (n): m < ↓n → ↑m < n.
 #m #n #H >(nlt_des_gen (𝟎) n)
 [ /2 width=1 by nlt_succ_bi/
-| /3 width=3 by le_nlt_trans, nlt_le_trans/
+| /3 width=3 by nle_nlt_trans, nlt_nle_trans/
 ]
 qed-.
 
+lemma nlt_inv_pred_bi (m) (n):
+      ↓m < ↓n → m < n.
+/3 width=3 by nlt_inv_pred_dx, nle_nlt_trans/
+qed-.
+
 (* Constructions with npred *************************************************)
 
 lemma nlt_zero_sn (n): n = ↑↓n → 𝟎 < n.