proposition: Lemma CRgball_plus (x x' y y': CR) e1 e2: ball e1 x x' -> ball e2 y y' -> ball (e1 + e2) (x + y)%CR (x' + y')%CR.
proof: Proof. Proof with auto. do 3 rewrite <- in_CRgball. intros [A B] [C D]. CRring_replace (x + y - ' (e1 + e2)%Q) (x - ' e1 + (y - ' e2)). CRring_replace (x + y + ' (e1 + e2)%Q) (x + ' e1 + (y + ' e2)). split; apply CRplus_le_compat... Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders