(* 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 →
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-.
(* 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 → ⊥.
#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.
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 ******************************************************)