Finish the construction of the structure of a field on reals

[valis]

There are several goals left in Arith.Real:

• [ ] The locatedness property for the product of two reals.
• [ ] The locatedness property for the inverse of a positive real.
• [ ] Various properties of the product, including associativity, commutativity, and distributivity.