x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ x + 0 < x + y
x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ 0 < y
conv_rhs => rw [← PartENat.add_lt_add_iff_left hx]
no goals
x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ x + 0 < x + y
rw [add_zero]