n m : Nat
H : n ∣ m
this : m % n + n * (m / n) = m
⊢ n * (m / n) = m
n m : Nat
H : n ∣ m
⊢ n * (m / n) = m
have := mod_add_div m n
no goals
n m : Nat
H : n ∣ m
this : m % n + n * (m / n) = m
⊢ n * (m / n) = m
rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this