Proof that classical reals are constructive reals with
extra properties, namely total order, existence of all
least upper bounds and setoid equivalence simplifying to
Leibniz equality.
From this point of view, the quotient Rabst and Rrepr
between classical Dedekind reals and constructive Cauchy reals
becomes an isomorphism for the ConstructiveReals structure.
This allows to apply results from constructive reals to
classical reals.