]
qed-.
-lemma le_ylt_trans (x) (y) (z): x ≤ y → yinj y < z → yinj x < z.
+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-.
]
qed-.
-lemma lt_ylt_trans (x) (y) (z): x < y → yinj y < z → yinj x < z.
+lemma lt_ylt_trans (x) (y) (z): x < y → yinj y < z → yinj x < z.
/3 width=3 by ylt_trans, ylt_inj/
qed-.