F : Type ?u.112908
α : Type ?u.112911
β : Type ?u.112914
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : R
n p : ℕ
hp : Even p
a : R
⊢ 0 ≤ a ^ p
F : Type ?u.112908
α : Type ?u.112911
β : Type ?u.112914
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : R
n p : ℕ
hp : Even p
a : R
⊢ abs a ^ p = a ^ p
rw [← abs_pow, abs_eq_self]
no goals
F : Type ?u.112908
α : Type ?u.112911
β : Type ?u.112914
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : R
n p : ℕ
hp : Even p
a : R
⊢ 0 ≤ a ^ p
exact hp.pow_nonneg _