no goals
α : Type ?u.27916
M₀ : Type ?u.27919
G₀ : Type u_1
M₀' : Type ?u.27925
G₀' : Type ?u.27928
F : Type ?u.27931
F' : Type ?u.27934
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a ≠ 0
⊢ 1 / a ≠ 0
simpa only [one_div] using inv_ne_zero h