proposition: Lemma n_Function_ball01_triangle : forall n e1 e2 f g h, (n_Function_ball01 n e1 f g) -> (n_Function_ball01 n e2 g h) -> (n_Function_ball01 n (e1+e2)%Q f h).
proof: Proof. induction n. apply ball_triangle. intros e1 e2 f g h H0 H1 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