fact: Definition Bsign x := match x with | B754_nan => false | B754_zero s => s | B754_infinity s => s | B754_finite s _ _ _ => s end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative