proposition: Lemma mspc_ball_CRplus_l (e : Q) (x y y' : CR) : ball e y y' -> ball e (x + y) (x + y').
proof: Proof. intro A. rewrite <- (rings.plus_0_l e). apply mspc_ball_CRplus; [| easy]. now apply mspc_refl. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.metric2.Metric CoRN.ode.metric CoRN.model.totalorder.QposMinMax MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.orders.orders MathClasses.orders.semirings MathClasses.orders.rings MathClasses.theory.rings CoRN.model.metric2.CRmetric CoRN.model.setoids.Qsetoid CoRN.model.metric2.Qmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRball CoRN.reals.fast.CRabs MathClasses.theory.abs MathClasses.orders.minmax