proposition: Lemma int_minus (f g : Q -> CR) `{@IsUniformlyContinuous Q (msp_mspc_ball Q_as_MetricSpace) CR (msp_mspc_ball CR) f f_mu, @IsUniformlyContinuous Q (msp_mspc_ball Q_as_MetricSpace) CR (msp_mspc_ball CR) g g_mu} (a b : Q) : @int (f - g) (@Integral_instance_0 (f-g) _ (@uc_ulc _ _ _ _ _ _ (@sum_uc Q (msp_mspc_ball Q_as_MetricSpace) (msp_mspc_ball_ext Q_as_MetricSpace) f (-g) _ _ _ _))) a b = int f a b - int g a b.
proof: Proof. rewrite int_plus. pose proof (int_negate g a b). transitivity (int f a b + - int g a b). apply ucFun2_wd. reflexivity. exact H1. 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