proposition: Lemma root_error_bnd : forall (e:Qpos) b, proj1_sig e <= 1 -> 1 <= b -> (root_has_error e b) -> b <= (2#1) + proj1_sig e.
proof: Proof. intros e b He Hb [H0 H1]. destruct Ha as [Ha0 Ha1]. rewrite -> Qle_minus_iff in *. assert (X:0 < 2 + b - proj1_sig e). apply Qlt_le_trans with 2. constructor. rewrite -> Qle_minus_iff. replace RHS with ((b + -(1)) + (1 + - proj1_sig e)) by (simpl; ring). Qauto_nonneg. replace RHS with ((((4#1) + - a) + (a + - (b - proj1_sig e)^2))/((2#1) + b - proj1_sig e)) by simpl; field; auto with *. apply Qle_shift_div_l. assumption. replace LHS with 0 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