m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m
m n : Nat
H : 0 < n
⊢ m * n / n = m
let t := add_mul_div_right 0 m H
no goals
m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m
rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t