fact: Definition Bfma_szero m (x y z : binary_float) := Bfma_szero prec emax m (B2BSN x) (B2BSN y) (B2BSN z).
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN