proposition: Lemma integral_additive' (a b : Q) (u v w : QnonNeg) : a + `u = b -> `u + `v = `w -> ∫ f a u + ∫ f b v = ∫ f a w.
proof: Proof. intros A1 A2. assert (QnonNeg.eq (u+v)%Qnn w) as H0 by apply A2. assert (Qeq (a+`u) b) as H1 by apply A1. transitivity ( ∫ f a u + ∫ f (a+`u) v). apply ucFun2_wd. reflexivity. rewrite <- A1. reflexivity. rewrite <- H0. 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 MathClasses.misc.propholds