Proving every positive natural number has unique predecessor I am independently working through Tao's Analysis I, and one of the exercises is to prove that every positive natural number has a unique predecessor. The actual lemma is (where $n++$ denotes the successor of $n$):

Let $a$ be a positive [natural] number. Then there exists exactly one natural number $b$ such that $b++=a$.

The hint given is to use induction, and the book uses the Peano axioms with $0\in\mathbb{N}$.
Here is my attempt at a proof, but I am not sure if I applied induction properly (I didn't seem to need the inductive hypothesis in proving the $k+1$ case), and I am even more unsure if uniqueness is proven:

The statement to prove is $(\forall a\not=0)(\exists!b)(b++=a)$, which is the same as $\forall a\exists!b(a\not=0\rightarrow (b++=a))$. Induction is used on $a$.
The basis step is to prove for $a=0$, which is $\exists!b(0\not=0\rightarrow (b++=0))$. Since the antecedent of the conditional is false, the statement is vacuously true. [But is $b$ unique...?]
For the inductive step, it is assumed that for an arbitrary $k$, $\exists!b(k\not=0\rightarrow (b++=k))$. Then $\exists!b((k++\not=0)\rightarrow (b++=k++))$ is to be derived. The second of these (the one being derived) can be rewritten as $(k++\not=0)\rightarrow (c++=k++)$, for some $c$.
$k++\not=0$ is true even without assuming it, since $0$ does not have a predecessor. But $c++=k++$ implies $c=k$ (because the successor function is injective), which shows that a [unique?] $c$ can be chosen such that it is equal to $k$. This closes the induction and thus every positive natural number has a unique successor.

My questions are: (1) Is this proof correct? (2) If the answer to the first question is 'no', is the general idea for the proof correct? (3) If the answers to both of the preceding questions are 'no', could someone point me in the right direction for a correct proof?
Any help would be appreciated. Thanks.
 A: As you have almost discovered yourself, things begin to slip right from the start whan you rewrite $\forall(a\ne0)\exists!b(b{+}\!{+}=a)$ to $\forall a\exists!b(a\ne0\rightarrow (b{+}\!{+}=a))$. The latter claim is not true because $\exists!b(0\ne 0\rightarrow \cdots)$ is false; there is more than one $b$ such that $(0\ne 0\to \cdots)$ is true.
I can't actually follow your reasoning in the induction step, but something seems to have gone very wrong by the time you argue "because the successor function is injective". Isn't that part of what you're trying to prove?
Most formulations of Peano Arithmetic do contain an explicit axiom saying something like $x{+}\!{+}=y{+}\!{+}\to x=y$, but you're not quoting the exact axioms you're using, so I can only guess that this might also be true for your system. In that case, I think it would be clearer to prove by induction that every nonzero number has at least one predecessor. When the dust has settled you can then add in uniqueness from the axiom at your leisure.
Done properly that way, you indeed don't need the induction hypothesis during the induction step -- this is usually a sign of something being amiss, but in this particular case it is actually all right. You are still getting something from the induction principle in the induction step, namely the assumption that the $a$ you are proving things about in the induction step is actually a successor. That happens to be the very fact you set out to prove, which explains why you didn't need the induction hypothesis in order to make progress.
A: Do induction on B and find that 0++ = n <=> 1=n, i think this proves the base and also works for uniqueness using axtiom number4.
Then assume B++ = N and Prove (B++)++ = N++, Again using axiom (4) u have that B++ = N which is what u assumed. Thus it is correct
Not sure if this proof is correct, sorry if i confuse instead of help.
A: I worked on this problem, and found no satisfactory answer on stackexchange, so continued to investigate. Proving basic things can be slippery and it's easy to make mistakes. I found clues in Proposition 0.2.3 on page 10 here and in an answer to the a question on the problem on Terence Tao's own blog on where Tao says "You can modify the statement of the exercise to an equivalent statement which makes sense for $a=0$. (The statement will probably look something like “For any natural number $a$, either $a=0$, or else there exists exactly one…”.)"
Following Tao's suggestion, modify as follows so we can use induction: For any natural number $a$, exactly one of these two statements is true: 1) $a=0$ or 2) there exists a unique natural number $b$ such that $b++=a$. To avoid introduction of confusing variables I rephrased equivalently as "statement 1) $a=0$ or statement 2) there is a unique natural number whose successor is $a$." Note that we must show one statement true and the other not true in each of the two induction steps, and also note that when using statement 2) we must prove both the existence and uniqueness of a natural number whose successor is $a$. Since all natural numbers except $0$ are positive by definition, the lemma we have set out to prove follows from statement 2).
Proceeding with induction, we  first verify the base case $a=0$,
i.e., we prove  $P(O)$. Statement 1) is true since $0=0$. Since no natural number has $0$ as its successor by axiom 2, statement 2) is not true. This proves our base case. Now suppose inductively that $a$ is a natural number, and $P(a)$ has already been proven. We must show $P(a++)$, i.e. 1) $a++=0$ or 2) there is a unique natural number whose successor is $a++$. Axiom 2 says since $a$ is a natural number that $a++$ ($a$'s successor by definition) is a natural number. If another number $c$ also has $a++$ as its successor, then $c=a$ by the contrapositive of axiom 4. Therefore there is a unique number, $a$, whose successor is $a++$ and statement 2) is true. Since $a++$ is never equal to zero by axiom 3, statement 1) is false. Thus our second induction step is proven and the proof is complete.
Missteps on my part would not be a surprise; as I mentioned before things get slippery at this basic level. Note that the second induction step as I have written it doesn't even use the assumption that $P(a)$ has already been proven, only that $a$ is a natural number! 
A: Anothe proof by induction.
We can rewrite the Lemma like this:
P(a):  "If a is a positive natural number, then there is a unique natural number whose successor is a."
For a = 0, P (a) is true because it has a false antecedent.
Suppose P (a) is true for some natural a.
Since a is a natural number, then a++ is also.         (Axiom 2.2)
If c is a natural number and c++ = a++, then c = a.   (Axiom 2.4)
So there is a single natural number whose successor is a++.
The Lemma is thus proved.
