rw [mul_comm]
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z ^ k' * z > 0
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h : z > 0
k' : ℕ
ih : z ^ k' > 0
h₂ : 0 < z * z ^ k'
⊢ z * z ^ k' > 0