no goals
x z y : Nat
H : 0 < y
⊢ (x + y * z) / y = x / y + z
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
no goals
case zero
x y : Nat
H : 0 < y
⊢ (x + y * zero) / y = x / y + zero
rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ succ (x / y + z) = x / y + succ z
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ (x + y * succ z) / y = x / y + succ z
rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]
no goals
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ succ (x / y + z) = x / y + succ z
rfl