have hodd := Nat.even_add_one.mp h₂
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
⊢ z ^ (k + 1) > 0
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
⊢ z ^ (k + 1) > 0