github.com/coq/opam-coq-archive
A formalisation of the IEEE754 norm on floating-point arithmetic
opam install coq-ieee754.8.10.0