R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m
rw [mul_comm]
no goals
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m
exact mod_add_div _ _