If we consider the natural numbers, we have for all $a,b\in\mathbb{N}$ that $a\leq b\Longleftrightarrow (\exists x\in\mathbb{N})[a+x=b]$. (For example if $a=2$ and $b=5$ there exists $3\in\mathbb{N}$ such that $2+3=5$.) Now, as a generalization of this I was trying to prove that if $(\mathbb{F},+,\cdot,\leq)$ is an ordered field, then for all $a,b\in \mathbb{F}$ we have that \begin{align*} a\leq b\Longleftrightarrow (\exists x\geq 0)[a+x=b]. \end{align*}
I've been using the following definitions: A field $(\mathbb{F}, +,\cdot)$ is called an ordered field iff there is an ordering relation $\leq$ on $\mathbb{F}$ such that for all $a,b,c\in \mathbb{F}$ we have \begin{align*} a\leq b\Longrightarrow a+c\leq b+c \end{align*} and \begin{align*} (0\leq a)\wedge (0\leq b)\Longrightarrow 0\leq a\cdot b, \end{align*} where an ordering is defined as a binary relation that's reflexive, anti-symmetric, and transitive.
Now, how do I get from my definitions to what I'm trying to prove?