Assume $0 \in \mathbb{N}$ and let $\sigma(n)$ be the successor of a $n \in \mathbb{N}$.
Definition. Let $+ : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$ be a map with the properties:
(1) $n + 0 = n$
(2) $m + \sigma(n) = \sigma(m + n)$
One can show that $0 + n = n$ and $n + 1 = 1 + n = \sigma(n)$.
Lemma. $\forall m,n \in \mathbb{N} : \sigma(m) + n = m + \sigma(n)$
Since it is an induction over multiple variables one has to show:
(1) $m=0, n=0$ (induction basis)
(2) $m \rightarrow \sigma(m)$ (induction step on m)
(3) $n \rightarrow \sigma(n)$ (induction step on n)
Base case ($m=n=0$)
$\sigma(0) + 0 = \sigma(0) = 0 + \sigma(0)\quad\checkmark$
Induction step ($n \rightarrow \sigma(n)$)
$\sigma(m) + \sigma(n) = \sigma(\sigma(m) + n) \overset{\text{base case}}{=} \sigma(m + \sigma(n)) = m + \sigma(\sigma(n)) \quad\checkmark$
Induction step ($m \rightarrow \sigma(m)$)
$\color{red}{\text{Here I get in trouble.}}$
$\sigma(\sigma(m)) + n ~\overset{?}{=}~ \sigma(m) + \sigma(n)$
I can't apply the definition or the induction basis on $\sigma(\sigma(m))$ when it is on the outer left. And I can't apply commutative or associative law since I need the lemma to proof these theorems.
How can I solve this problem?
Let us consider the following predicate about $n\in\Bbb N$: $$\tag{ $P$}\forall m\colon \sigma(m)+n=m+\sigma(n).$$
As $$m+\sigma(0)\stackrel{(2)}=\sigma(m+0)\stackrel{(1)}=\sigma(m)\stackrel{(1)}=\sigma(m)+0$$ for all $m$, we have shown that $P(0)$ holds.
Let $n\in\Bbb N$ and assume $P(n)$. Let $m\in\Bbb N$ be arbitrary. Then $$\sigma(m)+\sigma(n)\stackrel{(2)}=\sigma(\sigma(m)+n)\stackrel{P(n)}=\sigma(m+\sigma(n))\stackrel{(2)}=m+\sigma(\sigma(n)).$$ As $m$ was arbitrary, we have shown $P(\sigma(n))$.
As we have shown $P(0)$ and $\forall n\in\Bbb N\colon P(n)\to P(\sigma(n))$, we conclude that $\forall n\in\Bbb N\colon P(n)$, as was to be shown.