fact: Definition max x y := match (x ?= y)%float with | FEq | FGt => x | FLt => y | FNotComparable => nan end.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig