simp at h₂
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : z ^ k * 0 < z ^ k * z
⊢ z ^ k * z > 0
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : 0 < z ^ k * z
⊢ z ^ k * z > 0