Cannot prove Lemma 2.2.10 in Tao Analysis 1 Lemma 2.2.10 in Tao's Analysis 1 asks me to prove:

Let a be a positive number. Then there exists exactly one natural number b such that S(b) = a, where S is the successor function 

I attempt to prove existence only by induction as suggested.  I am trying to prove that $\forall a(a \ne 0 \Rightarrow \exists b(S(b) = a))$.  The base case $(a = 0)$ is true vacuously.  I then do the inductive step as follows:


*

*$a \ne 0 \Rightarrow \exists b(S(b) = a)$    (Assumption 1.)

*$S(a) \ne 0$  (Assumption 2)

*???

*$\exists b(S(b) = S(a))$

*$S(a) \ne 0 \Rightarrow\exists b(S(b) = S(a))$
etc.


I've got no idea what move needs to be made from line 3 onwards?  Can anyone help?
NOTE: I realize that someone has already posted a similar question here but I do not understand the answer given
 A: To prove $\forall a\,(a\neq 0\implies\exists b\,S(b)=a)$ by induction on $a$, you've already done the base case, $a=0$, by observing that the desired statement is vacuously true.  So here goes the induction step.  Assume the statement is true for $a$; we need to prove it for $S(a)$. That is, we need to prove that, if $S(a)\neq0$, then there is some $b$ such that $S(b)=S(a)$.  Well, that's pretty easy: $b=a$ works.  
(This induction proof is rather unusual, in that you don't actually need to use the induction hypothesis.)
A: To prove the existence only, it turns out you don;t need any of the Axioms! 
Here is a proof created in my Fitch prover: 

(Note that the system uses $x,y$ instead of $a,b$, since the latter are considered constants by the system. It also uses $s$ instead of $S$, since the latter would be considered a predicate, rather than a function by the system. Finally, the system has a built in Induction rule ... you can always just add the appropriate instance of the induction scheme, which in this case would be
$$(0 \not = 0 \rightarrow \exists b \ s(b) = 0) \land \forall a ((a \not = 0 \rightarrow \exists b \ s(b) = a) \rightarrow (s(a) \not = 0 \rightarrow \exists b \ s(b) = s(x)))) \rightarrow \forall a (a \not = 0 \rightarrow \exists b \ s(b) = a)$$
If you want to prove that there is a unique number $b$ such that $s(b)=a$, then you need to prove:

$\forall a(a \ne 0 \Rightarrow \exists b(S(b) = a \land \forall c (s(c) = a \rightarrow c = b)))$

For this, we need PA2: $\forall x \forall y (s(x) = s(y) \rightarrow x = y)$
Now, we can either do this all inside an inductive proof:

Or we can use the earlier established proof as a Lemma:

A: This theorem can be broken down into 2 parts.  (1) There exists at least 1 $b$ with the stated property and (2) There does not exist more than 1 $b$ with the stated property.
For (1), you can see from considering the structure $S = \{0, 1, 2, \dots\} \cup \{0.5, 1.5, 2.5, 3.5, \dots\}$ that $S$ satisfies the first order axioms of PA, but not the desired theorem, since $0.5$ doesn't have a predecessor.  So induction is required.  In this case, the inductive property that prevents $S$ from being a model of PA is straightforward, just the property that every nonzero value has a predecessor.
For (2), it turns out that the first order axioms of PA are enough to establish the theorem.  In fact, it follows directly from the axiom $x \ne y \to Sx \ne Sy$.  
