cases k with
| zero    => simp
| succ k' =>
  have ih := @powPos k' z h
  rw [pow_succ]
  have h₂ := arith_mul_pos_lt ⟨h, ih⟩
  simp at h₂
  rw [mul_comm]
  exact h₂
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h : z > 0
⊢ z ^ k > 0
no goals