match lt_trichotomy z 0 with
| Or.inl zNeg => exact powNegEven zNeg h₂
| Or.inr (Or.inl zZero) => rw [zZero] at h₁; simp at h₁
| Or.inr (Or.inr zPos)  => exact powPos zPos
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
⊢ z ^ k > 0
no goals