fact: Definition Bfrexp f := match f with | B754_finite s m e H => let e' := snd (Ffrexp_core_binary s m e) in (SF2B _ (proj1 (Bfrexp_correct_aux s m e H)), e') | _ => (f, (-2*emax-prec)%Z) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative