lemma yle_inv_succ1_lt: ∀x,y:ynat. ↑x ≤ y → 0 < y ∧ x ≤ ↓y.
#x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/
qed-.
lemma yle_inv_succ1_lt: ∀x,y:ynat. ↑x ≤ y → 0 < y ∧ x ≤ ↓y.
#x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/
qed-.