induction z with
| zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
| succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl
x z y : Nat
H : 0 < y
⊢ (x + y * z) / y = x / y + z
no goals