Prove that for all natural numbers $\neg\big(S(a)+b=a\big)$ The natural numbers are defined as per the Peano axioms.
Addition is defined recursively as follows:
$$
\begin{cases}
a + 0 &= a,\\
a + S(b) &= S(a+b).
\end{cases}
$$
Prove that $\forall a\forall b\Big(\neg\big(S(a)+b=a\big)\Big)$.

My attempts at a solution
I tried using induction on $b$, but I am struggling to prove the inductive step. Please do not use any laws regarding inequality, as I have yet to formally define them.
 A: We will use the following auxiliary results.
Lemma 1 $\forall b\forall a\big(a+S(b)=S(a)+b\big)$.
Proof We will proceed by induction on $b$.

*

*Base case. Assume that $b = 0$. We need to show that $\forall a\big(a+S(0)=S(a)+0\big)$. Let $a$ be a natural number. Then by the definition of addition $a+S(0) = S(a+0) = S(a) = S(a)+0$.


*Inductive step. Assume that for some natural number $b$ it holds that $\forall a\big(a+S(b)=S(a)+b\big)$. We will show that $\forall a\Big(a+S\big(S(b)\big)=S(a)+S(b)\Big)$. Let $a$ be a natural number. We need to show that $a+S\big(S(b)\big)=S(a)+S(b)$. In fact,
$$
\begin{align*}
a+S\big(S(b)\big) &= S\big(a+S(b)\big)\\
&= S\big(S(a)+b\big)\\
&= S(a)+S(b),
\end{align*}
$$
where the first and last equalities are by the definition of addition, and the remaining equality is by the induction hypothesis. $\square$
Lemma 2 $\forall b\forall a\big(S(a)+b=S(a+b)\big)$.
Proof We will prove this last claim by induction on $b$.

*

*Base case. We will prove that $\forall a\big(S(a)+0=S(a+0)\big)$. Let $a$ be a natural number. We need to show that $S(a)+0=S(a+0)$. In fact, $S(a)+0=S(a)=S(a+0)$: both equalities hold by the definition of addition.


*Inductive case. Assume that, for some natural number $b$, it holds that $\forall a\big(S(a)+b=S(a+b)\big)$. We will show that $\forall a\Big(S(a)+S(b)=S\big(a+S(b)\big)\Big)$. Let $a$ be a natural number. We need to show that $S(a)+S(b)=S\big(a+S(b)\big)$. In fact,
$$
\begin{align*}
S(a)+S(b) &= S\big(S(a)\big)+b\\
&= S\big(S(a)+b\big)\\
&= S\big(a+S(b)\big),
\end{align*}
$$
where the first and last equalities are by lemma 1, and the remaining equality is by the induction hypothesis. $\square$
Having proved the lemmas, we will now prove the desired statement, namely $\forall a\forall b\Big(\neg\big(S(a)+b=a\big)\Big)$. We will proceed by induction on $a$.

*

*Base case. Assume that $a=0$. We need to show that $\forall b\Big(\neg\big(S(0)+b=0\big)\Big)$. Let $b$ be a natural number. Then $S(0)+b=S(0+b)\neq 0$: the equality is by lemma 2, and the inequality is by the Peano axioms.


*Inductive step. Assume that for some natural number $a$ it holds that $\forall b\Big(\neg\big(S(a)+b=a\big)\Big)$. Define $a'=S(a)$. We will show that $\forall b\Big(\neg\big(S(a')+b=a'\big)\Big)$. We will proceed by reductio ad absurdum.
Suppose, to the contrary, that $b$ is a natural number such that $S(a')+b=a'$. Then, by lemma 2, $S(a'+b)=a'$, which is to say $S\big(S(a)+b\big)=S(a)$. Then, by the Peano axioms, $S(a)+b=a$, in contradiction to the induction hypothesis. $\square$

Remark My answer was originally written in accordance with the definition of addition given in the first edit of the question, whose recursive case was $a+S(b)=S(a)+b$. OP later changed the definition of addition so that the recursive case became $a+S(b)=S(a+b)$.
In order to adapt my answer to the revised definition, I decided, instead of starting from scratch, to keep my original proof, and simply add lemma 1.
If I'd written my original answer per the revised definition to begin with, it may have been different, and possibly shorter and simpler.
