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

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

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