have ih := @powPos k' z h
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
⊢ z ^ (k' + 1) > 0
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
⊢ z ^ (k' + 1) > 0