\section{Addition on 1-Based Natural Numbers is Cancellable}
Tags: Natural Numbers: 1-Based

\begin{theorem}
Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $+$ be addition on $\N_{>0}$.
Then:
:$\forall a, b, c \in \N_{>0}: a + c = b + c \implies a = b$
:$\forall a, b, c \in \N_{>0}: a + b = a + c \implies b = c$
That is, $+$ is cancellable on $\N_{>0}$.
\end{theorem}

\begin{proof}
By Ordering on $1$-Based Natural Numbers is Trichotomy, one and only one of the following holds:
:$a = b$
:$a < b$
:$b < a$
Suppose $a < b$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$a + c < b + c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this contradicts the fact that $a + c = b + c$.
Similarly, suppose $b > a$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$b + c < a + c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this also contradicts the fact that $a + c = b + c$.
The only other possibility is that $a = b$.
So 
:$\forall a, b, c \in \N_{>0}: a + c = b + c \implies a = b$
and so $+$ is right cancellable on $\N_{>0}$.
From Natural Number Addition is Commutative and Right Cancellable Commutative Operation is Left Cancellable:
:$\forall a, b, c \in \N_{>0}: a + b = a + c \implies b = c$
So $+$ is both right cancellable and left cancellable on $\N_{>0}$.
Hence the result.
{{qed}}
\end{proof}

