github.com/coq/opam-coq-archive
A Coq formalization of real analysis compatible with the standard library
opam install coq-coquelicot.2.1.1