no goals
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a✝ b✝ a b : α
⊢ (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
simp only [zpow_neg, zpow_one, mul_inv_rev]