%
\label{thm:mul-cancel-exactly-pos}
% Depends: I.D09, prop:integral-domain, prop:positive-closed
For $\underline{n} \in \tau\text{-Idx}$,
the following are equivalent:
\begin{enumerate}
    \item $\underline{n}$ satisfies multiplicative left-cancellation:
          $\underline{n} \times \underline{a}
           = \underline{n} \times \underline{b}
           \;\Rightarrow\;
           \underline{a} = \underline{b}$
          for all $\underline{a}, \underline{b}$.
    \item $\underline{n} > \underline{0}$.
\end{enumerate}

$(2) \Rightarrow (1)$.\;
Suppose $\underline{n} > \underline{0}$ and
$\underline{n} \times \underline{a}
 = \underline{n} \times \underline{b}$.
Then $\underline{n} \times (\underline{a} - \underline{b}) = \underline{0}$
in the sense that
$\underline{n} \times \underline{a}
 = \underline{n} \times \underline{b}$
implies (by the integral domain property,
Proposition~\ref{prop:integral-domain})
that either $\underline{n} = \underline{0}$ or
$\underline{a} = \underline{b}$.
Since $\underline{n} > \underline{0}$,
we conclude $\underline{a} = \underline{b}$.

$(1) \Rightarrow (2)$.\;
Contrapositive: if $\underline{n} = \underline{0}$,
then $\underline{0} \times \underline{1}
     = \underline{0}
     = \underline{0} \times \underline{2}$
but $\underline{1} \neq \underline{2}$
(Theorem~\ref{thm:mul-cancel-fails-zero}).