proposition: Theorem Bminus_correct : forall m x y, is_finite x = true -> is_finite y = true -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x - B2R y))) (bpow radix2 emax) then B2R (Bminus m x y) = round radix2 fexp (round_mode m) (B2R x - B2R y) /\ is_finite (Bminus m x y) = true /\ Bsign (Bminus m x y) = match Rcompare (B2R x - B2R y) 0 with | Eq => match m with mode_DN => orb (Bsign x) (negb (Bsign y)) | _ => andb (Bsign x) (negb (Bsign y)) end | Lt => true | Gt => false end else (B2SF (Bminus m x y) = binary_overflow m (Bsign x) /\ Bsign x = negb (Bsign y)).
proof: Proof. Proof with auto with typeclass_instances. intros m x y Fx Fy. generalize (Bplus_correct m x (Bopp y) Fx). rewrite is_finite_Bopp, B2R_Bopp. intros H. specialize (H Fy). rewrite <- Bsign_Bopp. destruct x as [| | |sx mx ex Hx], y as [| | |sy my ey Hy] ; try easy. now clear -Fy; destruct y as [ | | | ]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative