[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n✝ : ℤ
a : α
n : ℤ
⊢ (-a) ^ bit1 n = -a ^ bit1 n
[PROOFSTEP]
rw [zpow_bit1', zpow_bit1', neg_mul_neg, neg_mul_eq_mul_neg]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := h.exists_bit1
[GOAL]
case intro
α : Type u_1
inst✝ : DivisionRing α
a : α
k : ℤ
h : Odd (bit1 k)
⊢ (-a) ^ bit1 k = -a ^ bit1 k
[PROOFSTEP]
exact zpow_bit1_neg _ _
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
⊢ (-1) ^ n = -1
[PROOFSTEP]
rw [h.neg_zpow, one_zpow]
