fact: Definition Bdiv m x y := match x, y with | B754_nan, _ | _, B754_nan => B754_nan | B754_infinity sx, B754_infinity sy => B754_nan | B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy) | B754_finite sx _ _ _, B754_infinity sy => B754_zero (xorb sx sy) | B754_infinity sx, B754_zero sy => B754_infinity (xorb sx sy) | B754_zero sx, B754_infinity sy => B754_zero (xorb sx sy) | B754_finite sx _ _ _, B754_zero sy => B754_infinity (xorb sx sy) | B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy) | B754_zero sx, B754_zero sy => B754_nan | B754_finite sx mx ex _, B754_finite sy my ey _ => SF2B _ (proj1 (Bdiv_correct_aux m sx mx ex sy my ey)) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative