have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun))
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
⊢ z ^ (k + 1) < 0
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
⊢ z ^ (k + 1) < 0