]
qed-.
+lemma le_ylt_trans (x) (y) (z): x ≤ y → yinj y < z → yinj x < z.
+/3 width=3 by yle_ylt_trans, yle_inj/
+qed-.
+
lemma yle_inv_succ1_lt: ∀x,y:ynat. ↑x ≤ y → 0 < y ∧ x ≤ ↓y.
#x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/
qed-.
]
qed-.
+lemma lt_ylt_trans (x) (y) (z): x < y → yinj y < z → yinj x < z.
+/3 width=3 by ylt_trans, ylt_inj/
+qed-.
+
(* Elimination principles ***************************************************)
fact ynat_ind_lt_le_aux: ∀R:predicate ynat.