have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ 0 < z ^ (k' + 1)
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : z * z ^ k' > z * 0
⊢ 0 < z ^ (k' + 1)