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 α
inst✝ : HasDistribNeg α
x : α
n : ℤ
⊢ (-x) ^ bit0 n = x ^ bit0 n
rw [zpow_bit0', zpow_bit0', neg_mul_neg]