proposition: Lemma CRΣ_gball (f g: nat -> CR) (e : Q) (n : nat): (forall m, (m < n)%nat -> ball e (f m) (g m)) -> (ball (n * e) (@cmΣ CRasCMonoid n f) (@cmΣ CRasCMonoid n g)).
proof: Proof. induction n. - intros. apply ball_refl. rewrite Qmult_0_l. apply Qle_refl. - intros. rewrite Q.S_Qplus. setoid_replace ((n + 1) * e)%Q with (e + n * e)%Q by ring. unfold cmΣ. simpl @cm_Sum. apply CRgball_plus; auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal Coq.Unicode.Utf8 Coq.Program.Program CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.stdlib_omissions.N CoRN.ode.metric CoRN.ode.FromMetric2 CoRN.ode.SimpleIntegration