no goals
α : Type ?u.9473
M₀ : Type ?u.9476
G₀ : Type u_1
M₀' : Type ?u.9482
G₀' : Type ?u.9485
F : Type ?u.9488
F' : Type ?u.9491
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ c a b : G₀
h : b = 0 → a = 0
hb : b = 0
⊢ a * b / b = a
simp [*]