The constructive Cauchy real numbers, ie the Cauchy sequences
of rational numbers.
Cauchy reals are Cauchy sequences of rational numbers,
equipped with explicit moduli of convergence and
an equivalence relation (the difference converges to zero).
Without convergence moduli, we would fail to prove that a Cauchy
sequence of constructive reals converges.
Because of the Specker sequences (increasing, computable
and bounded sequences of rationals that do not converge
to a computable real number), constructive reals do not
follow the least upper bound principle.
The double quantification on p q is needed to avoid
forall un, QSeqEquiv un (fun _ => un O) (fun q => O)
which says nothing about the limit of un.
We define sequences as positive -> Q instead of nat -> Q,
so that we can compute arguments like 2^n fast.
WARNING: this module is not meant to be imported directly,
please import `Reals.Abstract.ConstructiveReals` instead.
WARNING: this file is experimental and likely to change in future releases.