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