+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.
+
+(* Properties on successor **************************************************)
+
+lemma ylt_O_succ: ∀n. 0 < ⫯n.
+* /2 width=1 by ylt_inj/
+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/
+qed.
+
+(* Properties on order ******************************************************)
+
+lemma yle_split_eq: ∀m:ynat. ∀n:ynat. m ≤ n → m < n ∨ m = n.