case intro
F : Type ?u.114094
α : Type ?u.114097
β : Type ?u.114100
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n k : ℕ
hk : n = 2 * k + 1
⊢ StrictMono fun a => a ^ n
F : Type ?u.114094
α : Type ?u.114097
β : Type ?u.114100
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
⊢ StrictMono fun a => a ^ n
cases' hn with k hk
no goals
case intro
F : Type ?u.114094
α : Type ?u.114097
β : Type ?u.114100
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n k : ℕ
hk : n = 2 * k + 1
⊢ StrictMono fun a => a ^ n
simpa only [hk, two_mul] using strictMono_pow_bit1 _