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