Terence Tao in his book Analysis I defines addition of two natural numbers like so:
- $0 + m := m$
- $ (n{++}) + m := (n+m){++}$
And later proves these two Lemmas:
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 later goes on to say "As a particular corollary of Lemma 2.2.2 and Lemma 2.2.3 we see that $n++=n+1$ (why?).".
This can be achieved using the Lemmas by setting $m=0$ on Lemma 2.2.3 and using Lemma 2.2.2 after that but couldn't it also be done without these Lemmas?
Proof. We use induction. The base case $n=0$ is true by the definition of the number $1$. Suppose inductively that the statement is true for $n$ i.e., $n++=n+1$ and we want to show that $(n++)++=(n++)+1$. By the I.H. the LHS can be written as $(n+1)++$ and by the definition of additon we can write RHS as $(n+1)++$. Which completes our induction. $$\tag*{$\blacksquare$}$$
This is my first encounter with books that rigorously prove all results and it felt weird to me why Tao chose to mention this corollary after the two lemmas and not before since if my proof is correct he could have mentioned it earlier. From the nature of this book and its axiomatic approach this threw me off, so either my proof is false or this isn't very important.
Best Answer
Don't think there is anything wrong with your proof. He could have chosen to write the corollary as a lemma before $2.2.2$ and $2.2.3$ and it will still make sense. It is a corollary here because it follows almost immediately from $2.2.2$ and $2.2.3$. Corollary does not mean that the result cannot be proven without its preceding theoreom/proposition/lemma as you have shown.