cases k with
| zero    => simp at h₂
| succ k' =>
  simp at h₂
  have k'Even := of_not_not (mt Nat.even_add_one.mpr h₂)
  have rc := powNegEven h₁ k'Even
  simp [Int.pow]
  have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
  simp at mulZ
  rw [pow_succ, mul_comm]
  exact mulZ
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Odd k
⊢ z ^ k < 0
no goals