proposition: Lemma integral_repeated_additive (a: Q) (b: QnonNeg) (n: nat): @cmΣ CRasCMonoid n (fun i: nat => ∫ f (a + i * ` b) b) == ∫ f a (from_nat n * b)%Qnn.
proof: Proof. unfold cmΣ. induction n; simpl @cm_Sum. assert (QnonNeg.eq (from_nat 0 * b)%Qnn 0%Qnn) by reflexivity. rewrite H. clear H. rewrite zero_width_integral. reflexivity. rewrite IHn. rewrite CRplus_comm. assert (QnonNeg.eq (from_nat (S n) * b)%Qnn (from_nat n * b + b)%Qnn). { change (S n * proj1_sig b == n * proj1_sig b + proj1_sig b)%Q. rewrite S_Qplus. ring. } rewrite H. clear H. apply integral_additive. 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