proposition: Lemma cmΣ_const (n : nat) (m : CR) : @cmΣ CRasCMonoid n (λ _, m) = m * '(n : Q).
proof: Proof. induction n as [| n IH]. - rewrite cmΣ_empty. simpl. rewrite CRmult_0_r. reflexivity. - rewrite cmΣ_succ. transitivity (m + (m*'n))%CR. apply ucFun2_wd. reflexivity. exact IH. clear IH. rewrite S_Qplus, <- CRplus_Qplus. rewrite CRmult_plus_distr_l. rewrite CRplus_comm. apply ucFun2_wd. reflexivity. rewrite CRmult_1_r. reflexivity. 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