Defining division when extending positive real numbers to real numbers Let us say that we have constructed the positive real numbers in some fashion (possibly including 0). Let us furthermore assume that we have defined addition and multiplication for ordered pairs of such numbers (an ordered pair $(x,y)$ is supposed to represent the difference $x-y$, but you cannot properly define subtraction for positive real numbers), and proved that these operations "work properly".
So we have reached the state where we have a ring $(K/\sim, +,\cdot)$ which extends $(\mathbb R^+,+,\cdot)$. Finally, let us assume that we already have division for $\mathbb R^+$. 
Now. How exactly do we show that multiplicative inverses exist, that is, that for any pair $(x,y)$ there exists a pair $(x',y')$ such that their product is equivalent to 1? Using the definition of multiplication for ordered pairs, we need to find $(x',y')$ such that $$(xx'+yy', xy'+x'y) \sim (1,0).$$
I have tried, but all I can get is that this reduces to $$x'-y' = \frac{1}{x-y}.$$
Unfortunately, as we still cannot actually subtract positive real numbers, this does not seem to help. 
One possible solution would be to show that having gotten this far, we can now actually subtract positive real numbers by using their isomorphic embedding in the extension. I have the feeling that this is the way to go, but I simply do not see how to write down a proof. It should be based on the following ordering of ordered pairs: $$(x,y)\le(x',y') \Leftrightarrow x+y'\le x'+y.$$
Basically, it seems we have to show somehow that expressions like $\sqrt2-\sqrt3$ (and also $\sqrt3-\sqrt2$!) make sense now.
 A: Why not just do it piecewise? For what it's worth, though, this might be a good reason to use an alternative, "sign-magnitude representation", instead of the difference-based representation, which is closer to how we typically work with signed numbers anyways and hence is more intuitive, or at least I think so. That is, if we are already given $\mathbb{R}^{+}$ by some alternative construction procedure, you can define an element of $\mathbb{R}$ to be
$$(\mbox{$+$ or $0$ or $-$}, m)$$
where the first item listed is the sign, to be one of the three symbols given, $m \in \mathbb{R}^{+}$ is the magnitude of the number, and we identify all elements of the form $(0, m)$ as being the same thing. Then just define
$$\frac{1}{x} := \left(s, \frac{1}{m}\right)$$
when $s \ne 0$, where we've done the right-hand reciprocal in the already-existing nonnegative reals. On the other hand, you have to now construct addition piecewise, but at least here it's considerably more obvious and natural how to do that (e.g. "plus plus minus is subtraction", etc.).
I don't think there's any good way to handle the difference-based definition that would not be piecewise - note that with the positive reals you can already subtract $x - y$ when $x > y$, and then just take $x - y$ for $x < y$ as $-(y - x)$. It works more slickly for building the additive group structure of the integers from the natural numbers, but not so much for the multiplicative structure of reals from positive reals. In particular, note that any "differencing" definition you are going to come up with has to mirror some operation on fractions of the form
$$\frac{a}{b} - \frac{c}{d}$$
which equals $\frac{ad - bc}{bd}$, but there's no way to get a difference in the denominator $bd$ without subtracting things there, i.e. using only addition, multiplication, and division of positive reals, and hence we're pretty much back to handling the case of the left operand being less than the right operand piecewisedly.
