case intro
F : Type ?u.107719
α : Type ?u.107722
β : Type ?u.107725
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a ≤ 0
k : ℕ
hk : n = 2 * k + 1
⊢ a ^ n ≤ 0
F : Type ?u.107719
α : Type ?u.107722
β : Type ?u.107725
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
ha : a ≤ 0
⊢ a ^ n ≤ 0
cases' hn with k hk
no goals
case intro
F : Type ?u.107719
α : Type ?u.107722
β : Type ?u.107725
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a ≤ 0
k : ℕ
hk : n = 2 * k + 1
⊢ a ^ n ≤ 0
simpa only [hk, two_mul] using pow_bit1_nonpos_iff.mpr ha