proposition: Lemma cmΣ_plus (n : nat) (f g : nat -> CR) : @cmΣ CRasCMonoid n (f + g) == @cmΣ CRasCMonoid n f + @cmΣ CRasCMonoid n g.
proof: Proof. induction n as [| n IH]. + symmetry. apply (@cm_rht_unit CRasCMonoid (@cmΣ CRasCMonoid 0 (f + g))). + rewrite cmΣ_succ. transitivity ((f + g)%mc n + (@cmΣ CRasCMonoid n f + @cmΣ CRasCMonoid n g))%CR. apply ucFun2_wd. reflexivity. exact IH. clear IH. rewrite cmΣ_succ. transitivity (f n + @cmΣ CRasCMonoid n f + (g n + @cmΣ CRasCMonoid n g))%CR. 2: reflexivity. do 2 rewrite CRplus_assoc. apply CRplus_eq_l. rewrite <- CRplus_assoc. rewrite <- (CRplus_comm (g n)), CRplus_assoc. apply CRplus_eq_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