Solution (source code)

= Solution

Fix $m$ and induct on $n$. At $n=0$,
$$
m^++0=m^+=(m+0)^+=m+0^+.
$$
If $m^++n=m+n^+$, then
$$
m^++n^+=(m^++n)^+=(m+n^+)^+=m+(n^+)^+.
$$
The last expression is the right-hand side required at the successor $n^+$. Therefore
$$
\boxed{m^++n=m+n^+\quad(m,n\in\omega).}
$$
In particular both sides also equal $(m+n)^+$ by the <recursion> equation for the second argument.