fact: Definition sign_FF x := match x with | F754_nan s _ => s | F754_zero s => s | F754_infinity s => s | F754_finite s _ _ => s end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN