Classical Dedekind reals. With the 3 logical axioms funext,
sig_forall_dec and sig_not_dec, the lower cuts defined as
functions Q -> bool have all the classical properties of the
real numbers.
We could prove operations and theorems about them directly,
but instead we notice that they are a quotient of the
constructive Cauchy reals, from which they inherit many properties.