Define $\leq\subset\Bbb{N}^2$ as follows: $$a<b\Leftrightarrow\exists:x\in\Bbb{N}:a+x=b$$ and $$a\leq b\Leftrightarrow a=b\vee a<b$$ Now, assume I've proven that $\leq$ is a partial order. Now, I wish to prove that $\leq$ is a total ordering on $\Bbb{N}$. Importantly, I'm working with 1-based natural numbers, that is $0\notin \Bbb{N}$. I'm working within Peano Axioms.
My go: I first present you with a lemma I'm using during the proof:
Lemma:$\forall a,b\in\Bbb{N}:a+b\neq 1$
We want to show that $\forall a,b\in \Bbb{N}:a\leq b \vee b\leq a$. The trivial case $a=b$ follows from antisymmetry, because then, we have $a\leq b$ and $b\leq a$. Now, assume $a\neq b$. We want to show that there is some $x_1\in \Bbb{N}$ such that $a+x_1=b$ or there is some $x_2\in \Bbb{N}$ such that $b+x_2=a$. We show that the first case holds if and only if the seconds doesn't thus always atleast one must hold (actually exactly one).
So, to prove $\Rightarrow$ Let there exist some $x_1\in \Bbb{N}$ such that $a+x_1=b$, we wish to show that $\forall x_2\in\Bbb{N}:b+x_2\neq a$. Substitute for $b$ in the second equation and add $1$ to both sides to obtain: $$a+x_1+x_2+1=a+1$$ which shows that $x_1+x_2+1\neq 1$ and that holds by the lemma.
Now in the part for $\Leftarrow$ im struggling: Assume that $\forall x_2\in \Bbb{N}:b+x_2\neq a$, we want to show that $\exists x_1\in \Bbb{N}:a+x_1=b$. Now, I have no idea how to explicitly find that $x_1$ when everything i know that this $x_2$ does NOT exist at all, i definitely cannot substitute the first equation into the second, because the first doesn't hold. Help please. Is this approach even correct?
By definition if $a\le b$ and $a\ne b$ we have $a<b$. If $a<b$ by definition $b=a+x$ for some natural $x$. Assuming $b\le a$ we have $b<a$ so $a=b+y$ for some natural $y$, hence $b=(b+y)+x=b+(y+x)>b$, contradiction, so no need the lemma.
And this is enough. Take $a,b$, if $b\le a$ and $a\le b$, assuming $a\ne b$, and using the exact same thing I did above you get contradiction.
If $a\le b$ and $b\le c$, if $b=a$ we are done, otherwise $b=a+d$ and then if $b=c$ we are done otherwise $c=b+g$ hence $c=a+d+g$ thus $a<c\implies a\le c$.
Given arbitrary $b$ we have $1\le b$. If $a\le b$ then $a+1\le b\lor b\le a+1$ thus for arbitrary $b$ we have $b\le a\lor a\le b$ for all $a.$