fact: Definition B2BSN (x : binary_float) : BinarySingleNaN.binary_float prec emax := match x with | B754_zero s => BinarySingleNaN.B754_zero s | B754_infinity s => BinarySingleNaN.B754_infinity s | B754_nan _ _ _ => BinarySingleNaN.B754_nan | B754_finite s m e H => BinarySingleNaN.B754_finite s m e H end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN