A corollary of two lemmas regarding the definition of addition of real numbers

Question

In Terence Tao's Analysis, he mentioned that two lemmas contribute to a corollary, which I can not fully understand.

To start with, Tao defined two axioms of addition:

1. 0 + m := m

2. (n++) + m := (n+m)++

And by this definition of addition we have

Lemma 2.2.2: For any natural number n, n + 0 = n

Lemma 2.2.3: For any natural number n and m, we have n + (m++) = (n+m) ++

And Tao continued to say these 2.2.2 and 2.2.3 implied n ++ = n + 1.

Now this is slightly confusing for me. In particular, I don't expect 1 to show up here. It seems to me that it should be a definition somehow. There may exist a number system where n ++ := n + a, n ++ := n + I, ...

Answer 1

Just take $m=0$ in lemma 2.2.3 and use lemma 2.2.2 to replace $n+0$ by $n$. You also need the definition of $1$ as mentioned in the comment.