- main proposition on lsx finally proved!

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_lt.ma

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 a306b57562a05fb302bbebad255f28ce61465a55..26135550e71f510781a6a03f19a09206b996503d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
@@ -122,6 +122,13 @@ lemma ylt_O: ∀x. ⫯⫰(yinj x) = yinj x → 0 < x.
 #H destruct
 qed.
 
+(* Properties on predecessor ************************************************)
+
+lemma ylt_pred: ∀m,n. m < n → 0 < m → ⫰m < ⫰n.
+#m #n * -m -n
+/4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/
+qed.
+
 (* Properties on successor **************************************************)
 
 lemma ylt_O_succ: ∀n. 0 < ⫯n.