rw [Nat.mul_div_assoc]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ a * b / c = a * (b / c)
case H
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ c ∣ b