proposition: Lemma rational_sqrt_mid_err : forall (e:Qpos), (proj1_sig e <= 1) -> root_has_error e (approximate rational_sqrt_mid e).
proof: Proof. intros e He. change (root_has_error e (sqrt_raw e)). unfold sqrt_raw. eapply root_has_error_le;[| |apply root_loop_error]. eapply Qle_trans;[apply He|]. apply root_loop_one_le; apply initial_root_one_le. apply Qpos_min_lb_r. apply initial_root_one_le. apply initial_root_error. clear. revert e. 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