It was given axiomatically, with classical set theory as the foundation. Define the reals as a complete, ordered field. In fact it can also be proven that any t

It was given axiomatically, with classical set theory as the foundation. Define the reals as a complete, ordered field. In fact it can also be proven that any two complete ordered fields are isomorphic. From this you can prove various cancellative, associative and distributive laws and obvious things like 0 < 1. See[0] for a readable Coq formalization. [0] https://www.cs.umd.edu/~rrand/vqc/Real.html https://www.cs.umd.edu/~rrand/vqc/Real.html