fact: Definition binary_fit_aux mode sx mx ex := if Zle_bool ex (emax - prec) then S754_finite sx mx ex else binary_overflow mode sx.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative