fact: Definition float_comparison_of_Xcomparison c := match c with | Xeq => FEq | Xlt => FLt | Xgt => FGt | Xund => FNotComparable end.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig