fact: Definition classify x := match classify x with | NaN => Sig.Fnan | PInf => Fpinfty | NInf => Fminfty | _ => Freal end.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig