cases k with
| zero    => simp
| succ k' =>
  have k'NotEven := Nat.even_add_one.mp h₂
  have k'Odd := Nat.odd_iff_not_even.mpr k'NotEven
  have rc := powNegOdd h₁ k'Odd
  simp [Pow.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₂ : Even k
⊢ z ^ k > 0
no goals