proposition: Lemma MVP_is_Bound01_plus : forall n M N p q, MVP_is_Bound01 n M p -> MVP_is_Bound01 n N q -> MVP_is_Bound01 n (M+N)%CR (p[+]q).
proof: Proof. induction n; intros M N p q Hp Hq. apply: AbsSmall_plus; auto. simpl. intros x Hx0 Hx1. rewrite -> plus_apply. auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.algebra.Bernstein CoRN.algebra.CRing_Homomorphisms CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.model.totalorder.QMinMax CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.reals.fast.CRabs CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.CRArith CoRN.reals.fast.CRArith_alg CoRN.algebra.RSetoid