fact: Definition Bsucc' x := match x with | B754_zero _ => Bldexp mode_NE Bone emin | B754_infinity false => x | B754_infinity true => Bopp Bmax_float | B754_nan => B754_nan | B754_finite false _ _ _ => Bplus mode_NE x (Bulp x) | B754_finite true _ _ _ => Bopp (Bpred_pos' (Bopp x)) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative