proposition: Lemma Qball_plus (e d: Q) (x x' y y': Q): Qball e x x' -> Qball d y y' -> Qball (e + d) (x + y) (x' + y').
proof: Proof. Proof with auto. intros. apply ball_triangle with (x' + y); apply Qball_Qabs. assert (Qeq (x + y - (x' + y)) (x - x')) by (simpl; ring). rewrite H1. clear H1. apply Qball_Qabs... assert (Qeq (x' + y - (x' + y')) (y - y')) by (simpl; ring). rewrite H1. apply Qball_Qabs... 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