proposition: Lemma initial_root_error : root_has_error (1#2) initial_root.
proof: Proof. destruct Ha as [Ha0 Ha1]. unfold initial_root, root_has_error. simpl. split. Qauto_le. rewrite -> Qle_minus_iff. assert (A0:(0<=1 + -((1#4)*a))). rewrite <- Qle_minus_iff. replace LHS with (a/(4#1)) by (simpl; field; discriminate). apply Qle_shift_div_r; try assumption. Qauto_pos. rewrite -> Qle_minus_iff in Ha0. replace RHS with ((a + -(1) + 1)*(1 +- ((1#4)*a))) by simpl; ring. 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