proposition: Lemma cmΣ_0 (f : nat -> CR) (n : nat) : (forall m, (m < n)%nat -> f m == 0) -> @cmΣ CRasCMonoid n f == 0.
proof: Proof. induction n as [| n IH]; intro H; [reflexivity |]. unfold cmΣ. simpl @cm_Sum. rewrite H by apply Nat.lt_succ_diag_r. rewrite IH; [apply CRplus_0_l |]. intros m H1; apply H. now apply Nat.lt_lt_succ_r. 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