proposition: Lemma root_has_error_ball : forall (e1 e2:Qpos) (b1 b2:Q), (proj1_sig e1 + proj1_sig e2<=1) -> (1 <= b1) -> (1 <= b2) -> root_has_error e1 b1 -> Qball (proj1_sig e2) b1 b2 -> root_has_error (e1+e2) b2.
proof: Proof. intros e1 e2 b1 b2 He Hb1 Hb2 [H0 H1] [H2 H3]. simpl in H2, H3. clear Ha. rewrite -> Qle_minus_iff in *. unfold root_has_error. autorewrite with QposElim. split; rewrite -> Qle_minus_iff. replace RHS with (((b1 + proj1_sig e1)^2 + - a) + (b2 + - (1) + proj1_sig e1 + proj1_sig e2 + (b1 + -(1)) + (2#1) + proj1_sig e1)*(proj1_sig e2 - (b1 - b2))) by simpl; ring. Qauto_nonneg. replace RHS with ((a + - (b1 - proj1_sig e1)^2) + (b1 - b2 + - - proj1_sig e2)*((b1 + -(1)) + (1 + - (proj1_sig e1 + proj1_sig e2)) + proj1_sig e2 + (b2 + -(1)) + (1 + - (proj1_sig e1 + proj1_sig e2)))) 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