fact: Definition FF2B x := match x as x return valid_binary x = true -> binary_float with | F754_finite s m e => B754_finite s m e | F754_infinity s => fun _ => B754_infinity s | F754_zero s => fun _ => B754_zero s | F754_nan b pl => fun H => B754_nan b pl H end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN