+lemma yle_antisym: ∀y,x. x ≤ y → y ≤ x → x = y.
+#x #y #H elim H -x -y
+/4 width=1 by yle_inv_Y1, yle_inv_inj, le_to_le_to_eq, eq_f/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma le_O1: ∀n:ynat. 0 ≤ n.
+* /2 width=1 by yle_inj/
+qed.
+
+lemma yle_refl: reflexive … yle.
+* /2 width=1 by le_n, yle_inj/
+qed.
+
+lemma yle_split: ∀x,y:ynat. x ≤ y ∨ y ≤ x.
+* /2 width=1 by or_intror/
+#x * /2 width=1 by or_introl/
+#y elim (le_or_ge x y) /3 width=1 by yle_inj, or_introl, or_intror/
+qed-.
+