X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_lt_pred.ma;h=e05ff9473f0c36213c42ded225f6108a4defff77;hp=cb776975830572cff409fe9e0317ef6d852ce584;hb=888840f6b3a71d3d686b53b702d362ab90ab0038;hpb=19b0a814861157ba05f23877d5cd94059f52c2e8

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 cb7769758..e05ff9473 100644
--- 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.