rw [zZero] at h₁
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : 0 ≠ 0
h₂ : Even k
zZero : z = 0
⊢ z ^ k > 0