proposition: Lemma pre_additive: (pre_result f a (ww true) + pre_result f (a+proj1_sig (ww true)) (ww false) == pre_result f a totalw)%CR.
proof: Proof. Proof with auto with *. intros. rewrite <- (uneven_CRplus_correct (ww true) (ww false)). simpl. apply regFunEq_equiv, regFunEq_e. intro e. simpl. unfold uneven_CRplus_approx. simpl. unfold approx. do 3 rewrite fastΣ_correct. apply added_summations. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal CoRN.stdlib_omissions.List Coq.Unicode.Utf8 Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.util.Qsums CoRN.model.metric2.Qmetric CoRN.model.setoids.Qsetoid CoRN.reals.fast.CRArith QnonNeg CoRN.util.Qgcd Coq.Program.Program CoRN.reals.fast.uneven_CRplus CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.tactics.Qauto CoRN.ode.metric CoRN.ode.FromMetric2 MathClasses.implementations.stdlib_rationals