Theorem: Nat.mul_add_div_right (Algdata/Init/Nat.lean)

State before:
x z y : Nat
⊢ y > 0 → (x * y + z) / y = x + z / y
Tactic:
intro h
State after:
x z y : Nat
h : y > 0
⊢ (x * y + z) / y = x + z / y

State before:
x z y : Nat
h : y > 0
⊢ (x * y + z) / y = x + z / y
Tactic:
rw [Nat.add_comm, Nat.add_mul_div_right z x h, Nat.add_comm]
State after:
no goals