proposition: Lemma sqrt_regular : is_RegularFunction Qball sqrt_raw.
proof: Proof. intros e1 e2. apply ball_weak_le with (proj1_sig (Qpos_min (1#2) e1 + Qpos_min (1#2) e2)%Qpos). - simpl. do 2 rewrite Q_Qpos_min. apply: plus_resp_leEq_both; simpl; auto with *. - apply ball_root_has_error. apply (Qle_trans _ (proj1_sig ((1#2) + (1#2))%Qpos)). 2: simpl; ring_simplify; apply Qle_refl. apply: plus_resp_leEq_both; apply Qpos_min_lb_l. apply root_loop_one_le. apply initial_root_one_le. apply root_loop_one_le. apply initial_root_one_le. apply root_loop_error. apply initial_root_one_le. apply initial_root_error. revert e1. intros [[n d] epos]. destruct n as [|n|n]. inversion epos. 2: inversion epos. apply root_max_steps. apply root_loop_error. apply initial_root_one_le. apply initial_root_error. revert e2. intros [[n d] epos]. destruct n as [|n|n]. inversion epos. 2: inversion epos. apply root_max_steps. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.reals.fast.CRpower CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.NRootIR CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.PowerBound CoRN.transc.RealPowers CoRN.reals.fast.ContinuousCorrect CoRN.tactics.Qauto CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra