proposition: Theorem sqrt_correct : forall prec, extension Xsqrt (sqrt prec).
proof: Proof. intros prec [ | xl xu] [ | x]; trivial; [now unfold convert; case (_ && _)|]. unfold convert. 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]. elim (F.sqrt_UP_correct prec xu); intros Vsuxu Hsuxu. unfold sqrt; rewrite F.cmp_correct, F.zero_correct, F'.classify_zero. generalize Vxl; rewrite F.valid_lb_correct. generalize (F.classify_correct xl); rewrite F.real_correct. case_eq (F.toX xl); [|intro rl]; intro Hrl. { now case F.classify; [easy|..|easy]; intros _ _; (rewrite F'.valid_lb_zero, Vsuxu; split; [rewrite F.zero_correct; apply sqrt_pos| revert Hxu Hsuxu; case (F.toX (F.sqrt_UP _ _)); [easy|intro rsxu]; case F.toX; [easy|intro rxu]; intro Hx; apply Rle_trans, sqrt_le_1_alt]). } revert Hxl. rewrite Hrl. intros Hxl. case F.classify; [|easy..]; intros _ _. unfold Xsqrt'. unfold Xcmp; case Rcompare_spec; intro Hrl0; rewrite Vsuxu; [rewrite F'.valid_lb_zero..|rewrite Bool.andb_comm]; simpl; [now split; [rewrite F.zero_correct; apply sqrt_pos|]; revert Hxu Hsuxu; case (F.toX (F.sqrt_UP _ _)); [easy|intro rsuxu]; case F.toX; [easy|intros rxu Hrxu]; apply Rle_trans, sqrt_le_1_alt..|]. elim (F.sqrt_DN_correct prec _ Vxl). intros Vslxl Hslxl. rewrite Vslxl. apply le_contains. { apply (le_lower_trans _ _ _ Hslxl). rewrite Hrl. simpl; unfold Xsqrt'. now apply Ropp_le_contravar, sqrt_le_1_alt. } revert Hsuxu. apply le_upper_trans. revert Hxu; xreal_tac2; intro Hxu; [exact I|]. simpl; unfold Xsqrt'. now apply sqrt_le_1_alt. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval