Intuitively it doesn't look to me that much of a research level problem but, if it's not too trivial, I think it needs a bit of careful thought to answer my question. I don't know whether the requirement "bit of careful thought" is enough to render it as a research level problem and that's why I am asking it here. If this question doesn't suit for this site, please let me know the answer in comments.
In standard treatment of Peano Axioms, say for example in Terence Tao's book Analysis I, the definition of $1$ is given right after stating the first two axioms, namely the following axioms,
Axiom 1. $0$ is a natural number.
Then Tao elaborates the notion of successors (the successor of $n$ is taken there as $n{++}$) and then states the following axiom,
Axiom 2. If $n$ is a natural number, then $n{++}$ is also a natural number.
After stating these two axioms he then gives the following definition,
Definition We define $0{++}=1$.
My objection is regarding the place of occurrence of this definition. In my opinion the definition shouldn't occur in the text until we have proved that $0{++}=1$. What do I mean by saying to prove $0{++}=1$? Let me elaborate the question a bit.
My argument is that the statement $0{++}=1$ of course can be taken as a definition of $1$ but only when we have proved the following property of our intuitive natural number system, loosely speaking, $$\color{blue}{\text{There doesn't exist any natural number between $0$ and $1$.}}$$ The necessity for proving this statement is that without it we cannot say that the construction of our natural number from Peano Axioms is complete (note that Axiom of Induction only excludes the existence of any other "non-natural" elements but so far as I know, it doesn't trivially exclude the possibility of having natural number between $0$ and $0{++}$). For if there really exists any natural number between $0$ and $0{++}$, the resulting system doesn't (apparently) contradicts any one of the Peano Axioms but still clearly it isn't the natural number system that we have known since our childhood and which is our objective to treat formally. And since one of the most important objective of this axiomatic treatment of natural number is to formalize our notion of natural numbers, we mustn't include in our formalized system any property that contradicts out intuitive notion of natural numbers. Otherwise the whole point of construction becomes meaningless.
Up untill now I can't find any rigorous proof of the fact that I have stated above and which, using logical operators becomes (all the variables indicating natural numbers), $$\not\exists b:0<b<0{++}$$
Is there any proof of this result? Can anyone elaborate where am I wrong?
I have discussed this problem with some of my friends but none of them could give me a satisfactory answer. I thought that maybe we should take this as an axiom. That's why I have posted it here to ask for the expert opinions.