proposition: Lemma root_has_error_le : forall (e1 e2:Qpos) (b:Q), proj1_sig e2 <= b -> proj1_sig e1 <= proj1_sig e2 -> root_has_error e1 b -> root_has_error e2 b.
proof: Proof. intros e1 e2 b Hb He [H0 H1]. rewrite -> Qle_minus_iff in *. split; rewrite -> Qle_minus_iff. replace RHS with (((b + proj1_sig e1) ^ 2 + - a) + (proj1_sig e2 + - proj1_sig e1)*((2#1) * (b + - proj1_sig e2 + proj1_sig e2) + proj1_sig e2 + proj1_sig e1)) by ring. Qauto_nonneg. replace RHS with ((a + - (b-proj1_sig e1)^2) + (proj1_sig e2 + -proj1_sig e1)*((proj1_sig e2 + - proj1_sig e1) + (2#1) * (b + - proj1_sig e2))) by 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