fact: Definition Bopp opp_nan x := match x with | B754_nan _ _ _ => build_nan (opp_nan x) | B754_infinity sx => B754_infinity (negb sx) | B754_finite sx mx ex Hx => B754_finite (negb sx) mx ex Hx | B754_zero sx => B754_zero (negb sx) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN