case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ 0 ≤ a ^ n ↔ 0 ≤ a
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ 0 ≤ a ^ n ↔ 0 ≤ a
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
⊢ 0 ≤ a ^ n ↔ 0 ≤ a
simpa only [hk, two_mul] using zpow_bit1_nonneg_iff