match Int.lt_trichotomy z 0 with
| Or.inl hneg => exact pow_neg_even hneg h₂
| Or.inr (Or.inl hzero) => rw [hzero] at h₁; simp at h₁
| Or.inr (Or.inr hpos)  => exact pow_pos hpos
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
⊢ z ^ k > 0
no goals