Using following definition of addition (Peano arithmetic):
Definition:$+:\Bbb{N}\times\Bbb{N}\rightarrow \Bbb{N}$ $$\forall a\in\mathbb{N}:a+1=s(a)\tag{i}$$ $$\forall a,b\in\mathbb{N}:a+s(b)=s(a+b)\tag{ii}$$
It is straghtforward to show that $+$ is well defined on $\mathbb{N}$. What I would like to prove is the following:$$\forall a,b,c\in\mathbb{N}:a=b\Leftrightarrow a+c=b+c$$ What seems logical to me that $\Leftrightarrow$ should hold, just by inspection. Many sources only mention $\Rightarrow$ hold. I am curious if it is NOT the case, that is, if my proof is wrong?
First, we prove that $a=b$ implies $a+c=b+c$. Let $a,b\in \Bbb{N}$ be arbitrary. Proceed by induction on $c$. Let $a=b$, then, $s(a)=s(b)$ we have that $a+1=b+1$ so the case $c=1$ holds. Let $a=b$ imply $a+c=b+c$. We wish to show that $a=b$ implies $a+s(c)=b+s(c)$. By induction premise we have that $a=b$ implies $a+c=b+c$, we apply $s$ to both sides to obtain: $s(a+c)=s(b+c)$. By ii. we have that $a+s(c)=b+s(c)$.
Now, we wish to prove that $a+c=b+c$ implies $a=b$. Let $a,b\in \Bbb{N}$ be arbitrary and proceed by induction on $c$. The case $c=1$ is: $a+1=b+1$ implies $s(a)=s(b)$ which, because $s$ is injective, implies $a=b$. Now consider $a+c=b+c$ impliying $a=b$. We wish to show that $a+s(c)=b+s(c)$ implies $a=b$. We see that $a+s(c)=b+s(c)$ is equivalent to saying $s(a+c)=s(b+c)$. So, by injectiveness, $a+c=b+c$ and by induction premise, we conclude that $a=b$.