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