no goals
α : Type ?u.10733
M₀ : Type ?u.10736
G₀ : Type u_1
M₀' : Type ?u.10742
G₀' : Type ?u.10745
F : Type ?u.10748
F' : Type ?u.10751
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c d a b : G₀
h : a = 0 → b = 0
⊢ a * b / a = b
rw [mul_comm, mul_div_cancel_of_imp h]