\begin{definition}[Definition:Addition/Peano Structure]
Let $\struct {P, 0, s}$ be a Peano structure.
The binary operation $+$ is defined on $P$ as follows:
:$\forall m, n \in P: \begin{cases}
m + 0 & = m \\
m + \map s n & = \map s {m + n}
\end{cases}$
This operation is called '''addition'''.
The definition can equivalently be structured:
:$\forall m, n \in P: \begin{cases}
0 + n & = n \\
\map s m + n & = \map s {m + n}
\end{cases}$
\end{definition}