Theorem: Nat.add_mul_div_right (Runtime/Utilities/Std.lean)

State before:
x y z : Nat
H : 0 < z
⊢ (x + y * z) / z = x / z + y
Tactic:
rw [Nat.mul_comm, add_mul_div_left _ _ H]
State after:
no goals