proposition: Lemma AQball_plus_l (ε : Qpos) (x y z : AQ_as_MetricSpace) : ball (proj1_sig ε) x y → ball (proj1_sig ε) (z + x) (z + y).
proof: Proof. intros E. apply AQball_abs. setoid_replace (z + x - (z + y)) with (x - y) 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