proposition: Lemma integrate_negate (f : Q -> CR) `{!IsUniformlyContinuous f f_mu} (a : Q) (w : QnonNeg) : ∫ (- f) a w = - ∫ f a w.
proof: Proof. apply ball_closed. intros e e_pos. mc_setoid_replace (0 + e) with e by ring. assert (he_pos : 0 < e / 2) by solve_propholds. destruct (integral_approximation (- f) a w (exist _ _ he_pos)) as [N1 F1]. destruct (integral_approximation f a w (exist _ _ he_pos)) as [N2 F2]. set (n := Pos.max N1 N2). assert (N1 <= n)%positive by apply Pos.le_max_l. assert (N2 <= n)%positive by apply Pos.le_max_r. setoid_replace e with (e/2+e/2)%Q. apply ball_triangle with (b:=riemann_sum (- f) a (proj1_sig w) n). - apply ball_sym, F1, H. - rewrite riemann_sum_negate. now apply mspc_ball_CRnegate, F2. - unfold Qdiv. rewrite <- Qmult_plus_distr_r. setoid_replace (/ 2 + / 2)%Q with 1%Q by reflexivity. rewrite Qmult_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 MathClasses.misc.propholds