proposition: Lemma MVP_uc_fun_close_left : forall n (e1 e2:Qpos) f1 f2 g, ball (proj1_sig e1) f1 f2 -> MVP_uc_fun_close_sig n (proj1_sig e2) f2 g -> MVP_uc_fun_close_sig n (proj1_sig e1+proj1_sig e2) f1 g.
proof: Proof. induction n; intros e1 e2 f g1 g2 H0 H1. eapply ball_triangle. apply H0. apply H1. intros x Hx0 Hx1. eapply IHn. apply H0; auto. apply H1; 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