I want to prove the following theorem:
Theorem 1: Let $a,b,c\in\mathbb{N}$, then $a+b\neq a$
using the following axiom
Axiom: There exists a set $\mathbb{N}$ with an element $1 \in\mathbb{N}$ and a function $s: \mathbb{N}\rightarrow\mathbb{N}$ that satisfy the following three properties.
There is no n $\in\mathbb{N}$ such that $s(n)=1$.
The function $s$ is injective.
Let $G\subseteq\mathbb{N}$ be a set. Suppose $1 \in G$, and that if g $\in G$ then $s(g)\in G$. Then $G=\mathbb{N}$.
and theorem
Theorem 1: There is a unique binary operation +: $\mathbb{N}\rightarrow\mathbb{N}$ that satisfies the following two properties for all n,m $\in\mathbb{N}$
1) $n+1=s(n)$
2) $n+s(m)=s(n+m)$
I have two proof ideas, and I do not know if they satisfy the "$g\in G\rightarrow s(g)\in G$" line of part 3 of the axiom.
My first idea was to consider a set $G=\{a\in\mathbb{N}:\forall b\in\mathbb{N}(a+b\neq a)\}$ and show that the contrapositve of $g\in G\rightarrow s(g)\in G$ is true, that is, $\neg(s(g)\in G)\rightarrow\neg(g\in G)$, but I do not know if changing the axiom like that is allowed.
My second idea was to show that $((g\in G)\land\neg(s(g)\in G))\rightarrow false$ which is shown here to be logically eqivalent to $g\in G\rightarrow s(g)\in G$. Again, I do not know if its okay to change the logical structure of an axiom.