proposition: Lemma mspc_ball_Qplus_l (e x y y' : Q) : @ball _ (msp_mspc_ball Q_as_MetricSpace) e y y' -> @ball _ (msp_mspc_ball Q_as_MetricSpace) e (x + y) (x + y').
proof: Proof. intro A. assert (A1 := radius_nonneg _ _ _ A). destruct (orders.le_equiv_lt _ _ A1) as [e_zero | e_pos]. - unfold ball. simpl. rewrite <- e_zero. unfold ball in A. simpl in A. rewrite <- e_zero in A. apply Qball_plus_r. apply A. - now apply Qball_plus_r. 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