+lemma yplus_O_sn: ∀n:ynat. 0 + n = n.
+#n >yplus_comm // qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma yplus_inv_inj: ∀z,y,x. x + y = yinj z →
+ ∃∃m,n. m + n = z & x = yinj m & y = yinj n.
+#z * [2: normalize #x #H destruct ]
+#y * [2: >yplus_Y1 #H destruct ]
+/3 width=5 by yinj_inj, ex3_2_intro/
+qed-.
+
+(* Properties on order ******************************************************)
+
+lemma yle_plus_dx2: ∀n,m. n ≤ m + n.
+* //
+#n elim n -n //
+#n #IHn #m >(yplus_succ2 ? n) @(yle_succ n) // (**) (* full auto fails *)
+qed.
+
+lemma yle_plus_dx1: ∀n,m. m ≤ m + n.
+// qed.
+
+(* Forward lemmas on order **************************************************)
+
+lemma yle_fwd_plus_sn2: ∀x,y,z. x + y ≤ z → y ≤ z.
+/2 width=3 by yle_trans/ qed-.
+
+lemma yle_fwd_plus_sn1: ∀x,y,z. x + y ≤ z → x ≤ z.
+/2 width=3 by yle_trans/ qed-.