(* 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-.