fact: Definition Bfma_szero m (x y z: binary_float) : bool := let s_xy := xorb (Bsign x) (Bsign y) in if Bool.eqb s_xy (Bsign z) then s_xy else match m with mode_DN => true | _ => false end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative