fact: Definition Bsucc x := match x with | B754_zero _ => B754_finite false 1 emin Bulp_correct_aux | B754_infinity false => x | B754_infinity true => Bopp Bmax_float | B754_nan => B754_nan | B754_finite false mx ex _ => SF2B _ (proj1 (binary_round_correct mode_UP false (mx + 1) ex)) | B754_finite true mx ex _ => SF2B _ (proj1 (binary_round_correct mode_ZR true (xO mx - 1) (ex - 1))) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative