fact: Definition Babs (x : binary_float) : binary_float := match x with | B754_nan => x | B754_infinity sx => B754_infinity false | B754_finite sx mx ex Hx => B754_finite false mx ex Hx | B754_zero sx => B754_zero false end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative