no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹
rw [mul_assoc, mul_inv_cancel ha, mul_one]
no goals
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
rw [← zpow_add_one₀ ha, sub_add_cancel]