How can I prove this proposition from Peano Axioms: (Cancellation law). Let a, b, c be natural numbers such that a + b = a + c. Then we have b = c. 
Peano Axioms.
Axiom 2.1
$0$ is a natural number.
Axiom 2.2
If $n$ is a natural number then $n++$ is also a natural number. (Here $n++$
  denotes the successor of $n$ and previously in the book the notational
  implication has been bijected to the familiar $1,2…$).
Axiom 2.3
$0$ is not the successor of natural number; i.e. we have $n++≠0$ for every
  natural number $n$.
Axiom 2.4
Different natural numbers must have different successors; i.e., if $n,m$
  are natural numbers and $n≠m$, then $n++≠m++$.
Axiom 2.5
Let $P(n)$ be any property pertaining to a natural number $n$. Suppose
  that $P(0)$ is true, and suppose that whenever $P(n)$ is true, $P(n++)$ is
  also true. Then $P(n)$ is true for every natural number $n$.
Definition of Addition: Let m be a natural number. We define, $0+m=m$
  and suppose we have inductively defined the addtion $n+m$ then we
  define, $(n++)+m=(n+m)++$. Where $n++$ is the successor of $n$.

Terence Tao has a proof in his Analysis I book, but I couldn't understand . I want a proof line by line like this:
Thm: 3 is a natural number 
\begin{align*}
   & 0 \text{ is natural } && \text{Axiom 2.1 }\\
   & 0++ = 1 \text{ is natural } && \text{Axiom 2.2}\\
   & 1++ = 2 \text{ is natural } && \text{Axiom 2.2}\\
   & 2++ = 3 \text{ is natural } && \text{Axiom 2.2}
   \end{align*}
 A: The proof is by induction on $a$.
Basis [case with $a=0$]. We want to prove that :

if $0+b=0+c$, then $b=c$.

But we have that : $0+b=b$, by definition of addition.
And also : $0+c=c$.
Thus, by transitivity of equality : $b=c$.

Induction step. Assume that the property holds for $a$ and prove it for $a'$ [I prefer to use $a'$ instead of $a++$ for the successor of $a$].
This means :

assume that "if $a+b=a+c$, then $b=c$" holds, and prove that "if $a'+b=a'+c$, then $b=c$" holds.

We have $a'+b=(a+b)'$ by definition of addition.
And $a'+c=(a+c)’$, by definition of addition.
We assume that : $a'+b=a'+c$, and thus, again by transitivity of equality, we have that : $(a+b)'=(a+c)'$.
By axiom 2.4 (different numbers have different successors), by contraposition, we conclude that $(a+b)=(a+c)$.
Thus, applying induction hypothesis, we have that :

$b=c$.



The general strategy used above in order to prove "if $P$, then $Q$", is to assume $P$ and derive $Q$.
This type of proof is called Conditional Proof; we can see it above :
1) if $a+b=a+c$, then $b=c$ --- induction hypothesis
2) $a'+b=a'+c$ --- assumption for CP
3) $(a+b)'=(a+c)'$ --- from 2) and definition of addition and tarnsitivity of equality
4) $a+b=a+c$ --- from 3) and axiom 2.4 by Contraposition [the axiom says : "if $(a+b \ne a+c)$, then $(a+b)' \ne (a+c)'$"; thus, contraposing it we get : "if $(a+b)' = (a+c)'$, then $(a+b) = (a+c)$"] and Modus ponens
5) $b=c$ --- from 4) and 1) by Modus ponens (also called : detachment)

6) if $a'+b=a'+c$, then $b=c$ --- from 2) and 5) by Conditional Proof.

A: Here is a formal proof done in Fitch:
(Note: I use $s(x)$ instead of $x$++)

