proposition: Theorem div_mixed_r_correct : forall prec yf, extension (fun x => Xdiv x (F.toX yf)) (fun xi => div_mixed_r prec xi yf).
proof: Proof. intros prec yf [| xl xu] [| x]; trivial; [now unfold convert; case (_ && _)|]. unfold convert at 1. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vxu Vxl. intros [Hxl Hxu]. simpl. generalize (F.classify_correct yf). rewrite F.cmp_correct, F.zero_correct, F.real_correct, F'.classify_zero. case_eq (F.classify yf); intro Cyf; [xreal_tac2; [easy|]|xreal_tac2; [|easy]..]; intros _; [|easy..]. unfold Xcmp. unfold Xdiv'. simpl. case Rcompare_spec ; intros Hy ; try exact I ; simpl; simpl_is_zero. { elim (F.div_DN_correct prec xu yf); [intros Vl Hl|]; last first. { unfold F.is_real_ub, F.is_real_lb, F.is_neg_real, F.is_pos_real. left. split. now destruct (F.toX xu). now rewrite X. } elim (F.div_UP_correct prec xl yf); [intros Vu Hu|]; last first. { unfold F.is_real_ub, F.is_real_lb, F.is_neg_real, F.is_pos_real. right. split. now destruct F.toX. now rewrite X. } rewrite Vl, Vu. split. { revert Hl; rewrite X. xreal_tac (F.div_DN prec xu yf); [now simpl|]. revert Hxu; xreal_tac xu; [now simpl|]; intro Hxu. unfold Xdiv, Xdiv'; simpl_is_zero. intro H; apply Ropp_le_cancel in H; revert H. unfold Rdiv ; eauto with mulauto. } revert Hu; rewrite X. xreal_tac (F.div_UP prec xl yf); [now simpl|]. revert Hxl; xreal_tac xl; [now simpl|]; intro Hxl. unfold Xdiv, Xdiv'; simpl_is_zero. unfold Rdiv ; eauto with mulauto. } elim (F.div_DN_correct prec xl yf); [intros Vl Hl|]; last first. { unfold F.is_real_ub, F.is_real_lb, F.is_neg_real, F.is_pos_real. right. split. now destruct (F.toX xl). now rewrite X. } elim (F.div_UP_correct prec xu yf); [intros Vu Hu|]; last first. { unfold F.is_real_ub, F.is_real_lb, F.is_neg_real, F.is_pos_real. left. split. now destruct (F.toX xu). now rewrite X. } rewrite Vl, Vu. split. { revert Hl; rewrite X. xreal_tac (F.div_DN prec xl yf); [now simpl|]. revert Hxl; xreal_tac xl; [now simpl|]; intro Hxl. unfold Xdiv, Xdiv'; simpl_is_zero. intro H; apply Ropp_le_cancel in H; revert H. unfold Rdiv ; eauto with mulauto. } revert Hu; rewrite X. xreal_tac (F.div_UP prec xu yf); [now simpl|]. revert Hxu; xreal_tac xu; [now simpl|]; intro Hxu. unfold Xdiv, Xdiv'; simpl_is_zero. unfold Rdiv ; eauto with mulauto. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval