have k'Even := of_not_not (mt Nat.even_add_one.mpr 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'Even : Even k'
⊢ z ^ (k' + 1) < 0