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

State before:
x z : Nat
H : 0 < z
⊢ (x + z) / z = succ (x / z)
Tactic:
rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
State after:
no goals