fact: Definition sign_SF x := match x with | S754_nan => false | S754_zero s => s | S754_infinity s => s | S754_finite s _ _ => s end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative