Farith, proved library for FloatingPoint computation

Farith

Coq documentation.