X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_lt.ma;h=a306b57562a05fb302bbebad255f28ce61465a55;hb=d95bd78c09617ad212fa9e96837a15fc907dcfca;hp=d30d6229dc48890aa90588d1a753494eb1e21d84;hpb=e2527c6784c2593ca67af35fafaf0b3725d80a60;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
index d30d6229d..a306b5756 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
@@ -98,8 +98,12 @@ lemma ylt_fwd_succ2: ∀m,n. m < ⫯n → m ≤ n.
 
 (* inversion and forward lemmas on yle **************************************)
 
+lemma ylt_fwd_le_succ1: ∀m,n. m < n → ⫯m ≤ n.
+#m #n * -m -n /2 width=1 by yle_inj/
+qed-.
+
 lemma ylt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n.
-#m #n * -m -n /3 width=1 by yle_pred_sn, yle_inj, yle_Y/
+#m #n * -m -n /3 width=1 by lt_to_le, yle_inj/
 qed-.
 
 lemma ylt_yle_false: ∀m:ynat. ∀n:ynat. m < n → n ≤ m → ⊥.
@@ -125,7 +129,7 @@ lemma ylt_O_succ: ∀n. 0 < ⫯n.
 qed.
 
 lemma ylt_succ: ∀m,n. m < n → ⫯m < ⫯n.
-#m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/ 
+#m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/
 qed.
 
 (* Properties on order ******************************************************)