induction k with
| zero    => simp [Int.pow_zero]
| succ k ih =>
  rw [Int.pow_succ]
  have h₂ := Int.mul_lt_mul_of_pos_left h ih
  simp at h₂
  exact h₂
a b c d : Int
k : Nat
z : Int
h : z > 0
⊢ z ^ k > 0
no goals