no goals
α : Type ?u.8508
M₀ : Type ?u.8511
G₀ : Type u_1
M₀' : Type ?u.8517
G₀' : Type ?u.8520
F : Type ?u.8523
F' : Type ?u.8526
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
hc : c ≠ 0
⊢ a / c * (c / b) = a / b
rw [← mul_div_assoc, div_mul_cancel _ hc]