proposition: Lemma rational_sqrt_mid_correct0 : (CRpower_N rational_sqrt_mid 2 == ' a)%CR.
proof: Proof. assert (H:AbsSmall (R:=CRasCOrdField) (' (3 # 1))%CR rational_sqrt_mid). split; simpl. intros e. change (-proj1_sig e <= sqrt_raw (Qpos2QposInf ((1#2)*e)) + - - (3#1)). apply Qle_trans with 0. rewrite -> Qle_minus_iff. ring_simplify. auto with *. rewrite <- Qle_minus_iff. apply Qle_trans with 1. discriminate. apply rational_sqrt_mid_one_le. intros e. change (-proj1_sig e <= 3 + - sqrt_raw (Qpos2QposInf ((1#2)*e))). apply Qle_trans with 0. rewrite -> Qle_minus_iff. ring_simplify. auto with *. rewrite <- Qle_minus_iff. apply rational_sqrt_mid_le_3. rewrite <- (CRpower_N_bounded_N_power 2 (3#1));[|assumption]. apply regFunEq_equiv, (regFunEq_e_small (X:=Q_as_MetricSpace) (CRpower_N_bounded 2 (3 # 1) rational_sqrt_mid) (' a)%CR (1#1)). intros e. destruct e as [[en ed] epos]. destruct en as [|en|en]. inversion epos. 2: inversion epos. set (e := exist (Qlt 0) (en # ed) epos). intro He. set (d:= (e * Qpos_inv (6#1))%Qpos). simpl (approximate (' a)%CR (Qpos2QposInf ((en # ed) ↾ epos))). change (Qball (proj1_sig e + proj1_sig e) (approximate ((CRpower_N_bounded 2 (3 # 1)) rational_sqrt_mid) (Qpos2QposInf e)) a). assert ( (approximate ((CRpower_N_bounded 2 (3 # 1)) rational_sqrt_mid) (Qpos2QposInf e)) = ((Qmax (- (3#1)) (Qmin (3#1) (approximate rational_sqrt_mid d)))^2) ) as H0. { simpl. replace d with (Qpos_mult e (Qpos_inv ((2 # 1) * (Qpos_power (3 # 1) (2 - 1)%positive)))). reflexivity. subst e d. apply Qpos_hprop. reflexivity. } rewrite H0. clear H0. setoid_replace (Qmin (3#1) (approximate rational_sqrt_mid d)) with ((approximate rational_sqrt_mid d)) by (rewrite <- Qle_min_r;destruct H;apply rational_sqrt_mid_le_3). setoid_replace (Qmax (-3#1) (approximate rational_sqrt_mid d)) with ((approximate rational_sqrt_mid d)) by (rewrite <- Qle_max_r;destruct H;eapply Qle_trans;[|apply rational_sqrt_mid_one_le];discriminate). assert (Z:root_has_error d (approximate rational_sqrt_mid d)). apply rational_sqrt_mid_err. unfold d. autorewrite with QposElim. change ((proj1_sig e/(6#1)) <= 1). apply Qle_shift_div_r. constructor. eapply Qle_trans. apply He. discriminate. set (z:=approximate rational_sqrt_mid d) in *. assert (X:z <= 3). apply rational_sqrt_mid_le_3. assert (X0:proj1_sig d^2 <= proj1_sig e). unfold d. autorewrite with QposElim in *. change ((proj1_sig e*(1#6))^2 <= proj1_sig e). rewrite -> Qle_minus_iff in *. replace RHS with (proj1_sig e*(1 + -proj1_sig e + (35#36)* proj1_sig e)) by simpl; ring. Qauto_nonneg. destruct Z; split; simpl; rewrite -> Qle_minus_iff in *; autorewrite with QposElim in *. replace RHS with (((z+proj1_sig d)^2 + - a) + (2#1) * ((3#1) + -z) * proj1_sig d + (proj1_sig e + - proj1_sig d^2)) by (simpl; unfold d;field;discriminate). Qauto_nonneg. replace RHS with (a + - (z-proj1_sig d)^2 + (2#1) * ((3#1) + - z)*proj1_sig d + proj1_sig d^2 + proj1_sig e) by (simpl; unfold d; autorewrite with QposElim;field;discriminate). Qauto_nonneg. 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