proposition: Lemma int_plus (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. unfold int; destruct (decide (a ≤ b)). rewrite integrate_plus. reflexivity. pose proof (integrate_plus f g b ((a - b) ↾ int_obligation_2 a b n)). rewrite H1. clear H1. apply rings.negate_plus_distr. 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