Theorem: Int.nat_mul_div_assoc' (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
⊢ a % c = 0 → a * b / c = a / c * b
Tactic:
intro hmod
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : a % c = 0
⊢ a * b / c = a / c * b

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : a % c = 0
⊢ a * b / c = a / c * b
Tactic:
rw [Nat.mul_comm, nat_mul_div_assoc hmod, Nat.mul_comm]
State after:
no goals