%
\label{prop:positive-closed}
For all $\underline{n}, \underline{m} \in \tau\text{-Idx}$:
\begin{enumerate}
    \item If $\underline{n} > \underline{0}$, then
          $\underline{n} + \underline{m} > \underline{0}$
          (addition preserves positivity).
    \item If $\underline{n} > \underline{0}$ and
          $\underline{m} > \underline{0}$, then
          $\underline{n} \times \underline{m} > \underline{0}$
          (multiplication preserves positivity).
    \item If $\underline{n} > \underline{0}$, then
          $\underline{n}^{\underline{m}} > \underline{0}$
          (exponentiation preserves positivity).
    \item $\underline{n} + \underline{1} > \underline{0}$ always
          (every successor is positive, with no guard needed).
\end{enumerate}

(1) $\underline{n} + \underline{m}
= \rho^m(\underline{n}) = \underline{n+m}$.
Since $n > 0$, we have $n + m \geq n > 0$.

(2) By induction on $\underline{m}$.
Base: $\underline{n} \times \underline{1} = \underline{n} > \underline{0}$.
Step: $\underline{n} \times (\underline{m+1})
= (\underline{n} \times \underline{m}) + \underline{n}$.
By the inductive hypothesis,
$\underline{n} \times \underline{m} > \underline{0}$,
so by~(1) the sum is positive.

(3) By induction on $\underline{m}$.
Base: $\underline{n}^{\underline{0}} = \underline{1} > \underline{0}$.
Step: $\underline{n}^{\underline{m+1}}
= \underline{n}^{\underline{m}} \times \underline{n}$.
By the inductive hypothesis and~(2), the product is positive.

(4) Special case of~(1):
$\underline{n} + \underline{1} = \underline{n+1} > \underline{0}$
for all $n \geq 0$.