rw [pow_succ, mul_comm]
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * z ^ k' < 0
⊢ z ^ (k' + 1) < 0
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even k'
rc : z ^ k' > 0
mulZ : z * z ^ k' < 0
⊢ z * z ^ k' < 0