[proofplan]
We prove the result constructively by induction on the first natural number $m$. In the base case $m=0$, a second induction on $n$ decides whether $0=n$ by reflexivity when $n=0$ and by disjointness of the zero and successor constructors when $n$ is a successor. In the successor step, we compare $S(k)$ with $n$ by cases on $n$: disjointness handles $n=0$, while the induction hypothesis decides equality of the predecessors when $n=S(\ell)$. Successor congruence transports a proof $k=\ell$ to a proof $S(k)=S(\ell)$, and successor injectivity transports any assumed equality $S(k)=S(\ell)$ back to $k=\ell$ in the negative branch.
[/proofplan]
[step:Define the decidability predicate to be proved by induction]
Define the predicate $D:\mathbb{N}\times\mathbb{N}\to\mathrm{Prop}$ by
\begin{align*}
D(m,n)\coloneqq (m=n)\vee\neg(m=n).
\end{align*}
It suffices to prove the proposition $P(m)$ for every $m\in\mathbb{N}$, where $P:\mathbb{N}\to\mathrm{Prop}$ is defined by
\begin{align*}
P(m)\coloneqq \forall n\in\mathbb{N}\,D(m,n).
\end{align*}
We use the induction principle for natural numbers on $m$.
[/step]
[step:Decide equality with zero by induction on the second argument]
We prove $P(0)$. Let $n\in\mathbb{N}$. We prove $D(0,n)$ by induction on $n$.
If $n=0$, then $0=0$ by reflexivity of equality, so the left disjunct of $D(0,0)$ holds.
If $n=S(\ell)$ for some $\ell\in\mathbb{N}$, then we prove the right disjunct. Let $h$ be an assumed proof of $0=S(\ell)$. This contradicts the constructor disjointness principle for natural numbers, namely that zero is not a successor. Hence $\neg(0=S(\ell))$, and therefore $D(0,S(\ell))$ holds.
Thus $D(0,n)$ holds for every $n\in\mathbb{N}$, so $P(0)$ holds.
[guided]
We must show that equality with $0$ is decidable for every natural number $n$. Define the auxiliary proposition $Q:\mathbb{N}\to\mathrm{Prop}$ by
\begin{align*}
Q(n)\coloneqq D(0,n).
\end{align*}
We prove $Q(n)$ for every $n\in\mathbb{N}$ by induction on $n$.
For the base case $n=0$, the proposition $Q(0)$ is
\begin{align*}
(0=0)\vee\neg(0=0).
\end{align*}
The equality $0=0$ is witnessed by reflexivity of equality. Therefore the left disjunct holds, and hence $D(0,0)$ holds.
For the successor case, let $\ell\in\mathbb{N}$ and suppose $n=S(\ell)$. The proposition to prove is
\begin{align*}
(0=S(\ell))\vee\neg(0=S(\ell)).
\end{align*}
The first disjunct cannot hold because the constructors $0$ and $S$ of the natural numbers are disjoint: no successor is equal to zero. To prove the second disjunct constructively, let $h$ be an arbitrary assumed proof of $0=S(\ell)$. By constructor disjointness, $h$ yields a contradiction. Since every assumed proof of $0=S(\ell)$ leads to contradiction, we have $\neg(0=S(\ell))$. Therefore the right disjunct holds, so $D(0,S(\ell))$ holds.
The induction on $n$ proves $D(0,n)$ for every $n\in\mathbb{N}$. This is exactly $P(0)$.
[/guided]
[/step]
[step:Reduce equality of successors to equality of predecessors]
Let $k\in\mathbb{N}$ and assume the induction hypothesis
\begin{align*}
H_k:\forall r\in\mathbb{N}\,D(k,r).
\end{align*}
We prove $P(S(k))$. Let $n\in\mathbb{N}$.
If $n=0$, then we prove $\neg(S(k)=0)$. Let $h$ be an assumed proof of $S(k)=0$. By symmetry of equality, $h$ gives a proof of $0=S(k)$, contradicting constructor disjointness. Hence $\neg(S(k)=0)$, so $D(S(k),0)$ holds.
If $n=S(\ell)$ for some $\ell\in\mathbb{N}$, apply $H_k$ to $\ell$. There are two cases.
If $H_k(\ell)$ gives a proof $p:k=\ell$, then applying congruence of the successor map $S:\mathbb{N}\to\mathbb{N}$ to $p$ gives a proof $S(k)=S(\ell)$. Hence $D(S(k),S(\ell))$ holds.
If $H_k(\ell)$ gives a proof $q:\neg(k=\ell)$, then we prove $\neg(S(k)=S(\ell))$. Let $h$ be an assumed proof of $S(k)=S(\ell)$. By successor injectivity, $h$ gives a proof $k=\ell$, contradicting $q$. Thus $\neg(S(k)=S(\ell))$, and $D(S(k),S(\ell))$ holds.
[/step]
[step:Conclude by induction on the first argument]
The base step proves $P(0)$, and the successor step proves $P(S(k))$ from $P(k)$ for every $k\in\mathbb{N}$. By the induction principle for natural numbers, $P(m)$ holds for every $m\in\mathbb{N}$. Expanding the definition of $P$, for every $m,n\in\mathbb{N}$ we obtain
\begin{align*}
(m=n)\vee\neg(m=n).
\end{align*}
This is the desired decidability of equality on natural numbers.
[/step]
