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