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