proposition: Lemma AQball_plus (ε1 ε2 : Qpos) (x1 x2 y1 y2 : AQ_as_MetricSpace) : ball (proj1_sig ε1) x1 y1 → ball (proj1_sig ε2) x2 y2 → ball (proj1_sig ε1 + proj1_sig ε2) (x1 + x2) (y1 + y2).
proof: Proof. intros. apply ball_triangle with (x2 + y1); apply AQball_abs. setoid_replace (x1 + x2 - (x2 + y1)) with (x1 - y1) by (simpl; ring). now apply AQball_abs. setoid_replace (x2 + y1 - (y1 + y2)) with (x2 - y2) by (simpl; ring). now apply AQball_abs. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring CoRN.util.Qdlog CoRN.model.totalorder.QposMinMax CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.metric2.MetricMorphisms CoRN.reals.faster.ApproximateRationals