This is a formalization of real numbers in Coq. Coq's standard library uses an axiomatic formalization. We instantiate one variant of it using two different approaches---Dedekind cut and Cauchy sequences.
Here is a list of modification that we made in the interface:
- Req is the equivalence between real numbers. It does not have to be Coq's equality. Arithmetic operators are required to preserve this equality.
- Trichotomous of real number ordering should not be computable.
- The floor function from R to Z should not be computable.