In message <firstname.lastname@example.org>, Dan Christensen <Dan_Christensen@sympatico.ca> writes >Something like that would work if there was some explicit link between >the field and order axioms. (The order axioms are usually given in >terms of positiveness, as in my proof, or in terms of various algebraic >rules, e.g. trichotomy.) How is this usually handled? I can't find >anything about this point on-line. It seems to me that ordering needs >to be defined in terms of addition. Or is there some clever little >lemma that is eluding me?
You have explicit links: "pos + pos = pos" and "pos * pos = pos".