I was wondering whether Coq defined the real numbers as Cauchy sequences or Dedekind cuts, so I checked Coq.Reals.Raxioms and... none of these two. The real numbers are axiomatized, along with their operations (as Parameters and Axioms). Why is it so?
Also, the real numbers tightly rely on the notion of subset, since one of their defining properties is that is every upper bounded subset has a least upper bound. The Axiom completeness encodes those subsets as Prop …