fact: Definition Bldexp mode f e := match f with | B754_finite sx mx ex _ => SF2B _ (proj1 (binary_round_correct mode sx mx (ex+e))) | _ => f end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative