fact: Definition binary_normalize mode m e szero := match m with | Z0 => B754_zero szero | Zpos m => SF2B _ (proj1 (binary_round_correct mode false m e)) | Zneg m => SF2B _ (proj1 (binary_round_correct mode true m e)) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative