rw [Nat.mul_comm, Nat.mul_add_div this, (Nat.div_eq_zero_iff this).mpr hy]
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ (x * n + y) / n = x
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ x + 0 = x