no goals
α : Type ?u.26175
M₀ : Type ?u.26178
G₀ : Type u_1
M₀' : Type ?u.26184
G₀' : Type ?u.26187
F : Type ?u.26190
F' : Type ?u.26193
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹
simp [mul_inv_rev]