In another proof of mine I had written:
Since $d \neq 0$ we can write $S(k) = d$ for some $k$ without violating Peano's 3rd axiom.
Apparently this isn't a valid step in a proof so I want to more explicitly prove that
$\forall x (x \not = 0 \rightarrow \exists y : S(y) = x)$
where $S$ is the successor function.
I wish to prove this via induction.
Now I don't know technically what kind of induction I am allowed to use, since Peano's 5th axiom is more like "For any property $P$ of a natural number, if $P(0)$ holds and $P(k)$ implies $P(k+1)$ then $P(n)$ is true for every natural number $n$."
So I need my base case to be a $k=0$ case, but since $x \neq 0$ I don't know if I am allowed to induct on $x$ starting at $1$. But even if I am I am not sure how to prove it correctly since it's a very different type of proof than what I am used to.
Base Case: Let $x=1$. Then $y=0$ satisfies $S(y) = S(0) = 1$.
Inductive Step: Suppose there exists a $z$ such that $S(z) = x$. We must show that there exists a $y$ such that $S(y) = S(x)$. By Peano's 4th axiom (which states that if $m=n$ then $S(m)=S(n)$), we have $S(S(z)) = S(x)$. If we let $y=S(S(z))=x$, we are done.
Is this correct? Am I even allowed to do this? Does this even prove what I want to prove?