github.com/coq/opam-coq-archive
Mathematical Components Library on real closed fields
opam install coq-mathcomp-real-closed.1.0.4