+(* Basic properties *********************************************************)
+
+lemma ylt_O: ∀x. ⫯⫰(yinj x) = yinj x → 0 < x.
+* /2 width=1 by/ normalize
+#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.
+