fact: Definition Bnearbyint md (x : binary_float) := match x with | B754_nan => B754_nan | B754_zero s => B754_zero s | B754_infinity s => B754_infinity s | B754_finite s m e H => SF2B _ (proj1 (Bnearbyint_correct_aux md s m e H)) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative