proposition: Lemma Qball_plus_r (e: Q) (x y y': Q): Qball e y y' -> Qball e (x + y) (x + y').
proof: Proof. Proof with auto. intros B. apply Qball_Qabs. apply Qball_Qabs in B. assert (Qeq (x + y - (x + y')) (y - y')) by (simpl; ring). rewrite H. exact B. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals