fact: Definition B2SF x := match x with | B754_finite s m e _ => S754_finite s m e | B754_infinity s => S754_infinity s | B754_zero s => S754_zero s | B754_nan => S754_nan end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative