have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) h₁
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
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : z * z ^ k > z * 0
⊢ z ^ (k + 1) > 0