Foundations of analysis - Natural number addition operator proof/definition In Landau's "Grundlagen der Analysis" the author states the following proposition which at the same time is a definition.
$$\text{Proposition 4/at the same time Definition 1. There is precisely one way to define an operation}$$
$$+: \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}, (x, y) \mapsto +(x, y) := x + y :=  (x + 1 = x' \quad \land \quad x + y' = (x + y)'.
$$
Where $'$ is the successor function of a natural number.
In Tao's Analysis I, the author just takes the operation of addition as a definition without proving existence and uniqueness (with the difference that Tao uses $0$ as the smallest natural number and Landau uses $1$). 
Since when do we have to prove definitions? Proving a definition is new to me.
 A: Sometimes when making a mathematical definition, there is some choice. You have mentioned one such situation: open one book, and the natural numbers include zero. Open another book, and zero is not an element of the natural numbers.
In Landau's booklet, the theorem you mention shows that there is no choice for the definition of natural-number addition $x+y$, if we insist on two rather mild requirements. (Requirements to which no one will object, given the intuitive notion "successor" and our experience of ordinary, primitive counting.)
Landau might have written the definition explicitly, but if he had done so, it would read something like the following.

We define $+:N \times N \to N$ in the only way that it can be defined, in accordance with the previous theorem.

In summary, Landau is not "proving a definition". As always, definitions are arbitrary and subject to the court of popularity.
Remark 1: In proving the Commutative Law of Addition a few pages later, Landau calls upon the proof of Proposition 4. The proof is part of the greater development.
Remark 2: In the prefaces, Landau discusses Proposition 4 in relation to the Peano axioms, and relates his story of how it came to be included in his development.
