case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ a ^ n < 0 ↔ a < 0
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0
cases' hn with k hk
no goals
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ a ^ n < 0 ↔ a < 0
simpa only [hk, two_mul] using zpow_bit1_neg_iff