+lemma ylt_plus1_to_minus_inj2: ∀x,z:ynat. ∀y:nat. x + y < z → x < z - y.
+#x #z #y #H lapply (monotonic_ylt_minus_dx … H y ?) -H //
+qed-.
+
+lemma ylt_plus1_to_minus_inj1: ∀x,z:ynat. ∀y:nat. y + x < z → x < z - y.
+/2 width=1 by ylt_plus1_to_minus_inj2/ qed-.
+
+lemma ylt_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. z ≤ x → x < y + z → x - z < y.
+/2 width=1 by monotonic_ylt_minus_dx/ qed-.
+
+lemma ylt_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. z ≤ x → x < z + y → x - z < y.
+/2 width=1 by ylt_plus2_to_minus_inj2/ qed-.
+