proposition: Lemma root_step_error : forall b (e:Qpos), (1 <= b) -> (proj1_sig e <= 1) -> root_has_error e b -> root_has_error ((1#2)*(e*e)) (root_step b).
proof: Proof. intros b e Hb He [H0 H1]. unfold root_step. assert (A0:0 < b). apply Qlt_le_trans with 1; try assumption. Qauto_pos. assert (A1:(0 <= b - proj1_sig e^2)). replace RHS with (b + - proj1_sig e^2) by simpl; ring. rewrite <- Qle_minus_iff. apply Qle_trans with ((1:Q)[^]2); try assumption. replace LHS with ((proj1_sig e)[^]2) by (simpl; ring). apply: (power_resp_leEq);simpl; try assumption. apply Qpos_nonneg. assert (A2:(0 <= a)). eapply Qle_trans;[|apply H1]. replace RHS with ((b-proj1_sig e)[^]2) by (simpl; ring). apply: sqr_nonneg. split. apply Qle_trans with ((b / (2#1) + a / ((2#1) * b))^2); [|Qauto_le]. field_simplify (b / (2#1) + a / ((2#1) * b)); auto with *. rewrite -> Qdiv_power. apply Qle_shift_div_l. Qauto_pos. rewrite -> Qle_minus_iff. replace RHS with ((b^2 - a)[^]2) by (simpl; ring). apply: sqr_nonneg. field_simplify (b / (2#1) + a / ((2#1) * b) - ((1#2)*proj1_sig (e * e)%Qpos)); auto with *. rewrite -> Qdiv_power. apply Qle_shift_div_r. Qauto_pos. replace LHS with ((a + b^2 - b*proj1_sig e^2)^2) by simpl; ring. apply Qle_trans with ((a + b^2 - proj1_sig e^2)^2). replace RHS with ((a + b ^ 2 - proj1_sig e ^ 2)[^]2) by (simpl; ring). replace LHS with ((a + b ^ 2 - b * proj1_sig e ^ 2)[^]2) by (simpl; ring). apply: (power_resp_leEq). replace RHS with (a + b*(b-proj1_sig e^2)) by simpl; ring. Qauto_nonneg. rewrite -> Qle_minus_iff;ring_simplify. replace RHS with ((b-1)*((proj1_sig e)[^]2)) by (simpl; ring). rewrite -> Qle_minus_iff in Hb. Qauto_nonneg. rewrite -> Qle_minus_iff. replace RHS with ((a-(b-proj1_sig e)^2)*((b+proj1_sig e)^2-a)) by simpl; ring. rewrite -> Qle_minus_iff in *|-. apply: mult_resp_nonneg; assumption. 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