proposition: Theorem Bdiv_correct : forall m x y, B2R y <> 0%R -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then B2R (Bdiv m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\ is_finite (Bdiv m x y) = is_finite x /\ (is_nan (Bdiv m x y) = false -> Bsign (Bdiv m x y) = xorb (Bsign x) (Bsign y)) else B2SF (Bdiv m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
proof: Proof. intros m x [sy|sy| |sy my ey Hy] Zy ; try now elim Zy. revert x. unfold Rdiv. intros [sx|sx| |sx mx ex Hx] ; try ( rewrite Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ simpl ; try easy ; now rewrite B2R_build_nan, is_finite_build_nan, is_nan_build_nan | apply bpow_gt_0 | auto with typeclass_instances ] ). simpl. case Bdiv_correct_aux. intros H1. unfold Rdiv. case Rlt_bool. intros (H2, (H3, H4)). split. now rewrite B2R_SF2B. split. now rewrite is_finite_SF2B. rewrite Bsign_SF2B. congruence. intros H2. now rewrite B2SF_SF2B. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative