proposition: Lemma QAbsSmall_plus : forall e1 e2 x1 x2 : Q, QAbsSmall e1 x1 -> QAbsSmall e2 x2 -> QAbsSmall (e1+e2) (x1+x2).
proof: Proof. intros. pose proof (@Qball_plus e1 e2 x1 0 x2 0). unfold Qball, QAbsSmall, Qminus in H1. do 4 rewrite Qplus_0_r in H1. apply H1. exact H. exact H0. 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