fact: Definition Bplus m x y := match x, y with | B754_nan, _ | _, B754_nan => B754_nan | B754_infinity sx, B754_infinity sy => if Bool.eqb sx sy then x else B754_nan | B754_infinity _, _ => x | _, B754_infinity _ => y | B754_zero sx, B754_zero sy => if Bool.eqb sx sy then x else match m with mode_DN => B754_zero true | _ => B754_zero false end | B754_zero _, _ => y | _, B754_zero _ => x | B754_finite sx mx ex Hx, B754_finite sy my ey Hy => let ez := Z.min ex ey in binary_normalize m (Fplus_naive sx mx ex sy my ey ez) ez (match m with mode_DN => true | _ => false end) end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative