cases k with
| zero    => simp [Int.pow_zero]
| succ k =>
  have hodd := Nat.even_add_one.mp h₂
  have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) 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 = 0
⊢ z ^ k > 0
no goals