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