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