github.com/coq/opam-coq-archive
Real numbers as coinductive ternary streams
opam install coq-coinductive-reals.8.10.0