have k'NotEven := Nat.even_add_one.mp h₂
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
⊢ z ^ (k' + 1) > 0
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
⊢ z ^ (k' + 1) > 0