R : Type u
inst✝ : EuclideanDomain R
a b : R
b0 : b ≠ 0
⊢ b * a / b = a
R : Type u
inst✝ : EuclideanDomain R
a b : R
b0 : b ≠ 0
⊢ a * b / b = a
rw [mul_comm]
no goals
R : Type u
inst✝ : EuclideanDomain R
a b : R
b0 : b ≠ 0
⊢ b * a / b = a
exact mul_div_cancel_left a b0