no goals
α : Type ?u.8170
M₀ : Type ?u.8173
G₀ : Type u_1
M₀' : Type ?u.8179
G₀' : Type ?u.8182
F : Type ?u.8185
F' : Type ?u.8188
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
hc : c ≠ 0
⊢ a / c / (b / c) = a / b
rw [div_div_eq_mul_div, div_mul_cancel _ hc]