case intro
F : Type ?u.106364
α : Type ?u.106367
β : Type ?u.106370
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : R
n : ℕ
a : R
k : ℕ
hk : n = k + k
⊢ 0 ≤ a ^ n
F : Type ?u.106364
α : Type ?u.106367
β : Type ?u.106370
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n
cases' hn with k hk
no goals
case intro
F : Type ?u.106364
α : Type ?u.106367
β : Type ?u.106370
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : R
n : ℕ
a : R
k : ℕ
hk : n = k + k
⊢ 0 ≤ a ^ n
simpa only [hk, two_mul] using pow_bit0_nonneg a k