- 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 265572bae8f8caf27aef92d6b681eea17969ef70..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
@@ -26,10 +26,14 @@ interpretation "ynat 'less than'" 'lt x y = (ylt x y).
 
 (* Basic forward lemmas *****************************************************)
 
-lemma ylt_inv_gen: ∀x,y. x < y → ∃m. x = yinj m.
+lemma ylt_fwd_gen: ∀x,y. x < y → ∃m. x = yinj m.
 #x #y * -x -y /2 width=2 by ex_intro/
 qed-.
 
+lemma ylt_fwd_le_succ: ∀x,y. x < y → ⫯x ≤ y.
+#x #y * -x -y /2 width=1 by yle_inj/
+qed-.
+
 (* Basic inversion lemmas ***************************************************)
 
 fact ylt_inv_inj2_aux: ∀x,y. x < y → ∀n. y = yinj n →
@@ -51,7 +55,7 @@ lemma ylt_inv_inj: ∀m,n. yinj m < yinj n → m < n.
 qed-.
 
 lemma ylt_inv_Y1: ∀n. ∞ < n → ⊥.
-#n #H elim (ylt_inv_gen … H) -H
+#n #H elim (ylt_fwd_gen … H) -H
 #y #H destruct
 qed-.
 
@@ -94,8 +98,12 @@ lemma ylt_fwd_succ2: ∀m,n. m < ⫯n → m ≤ n.
 
 (* inversion and forward lemmas on yle **************************************)
 
-lemma lt_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/
+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 lt_to_le, yle_inj/
 qed-.
 
 lemma ylt_yle_false: ∀m:ynat. ∀n:ynat. m < n → n ≤ m → ⊥.
@@ -114,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.
@@ -121,7 +136,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 ******************************************************)