cases k with
| zero    => simp at h₂
| succ k =>
  have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun))
  have mulZ : z * 0 > z * z ^ k := Int.mul_lt_mul_of_neg_left (pow_neg_even h₁ heven) h₁
  simp at mulZ
  rw [Int.pow_succ, Int.mul_comm]
  exact mulZ
a b c d : Int
k : Nat
z : Int
h₁ : z < 0
h₂ : k % 2 = 1
⊢ z ^ k < 0
no goals