proposition: Lemma Integrable_proper_l (f g: Q → CR) {fint: Integral f}: canonical_names.equiv f g → Integrable f → @Integrable g fint.
proof: Proof. Proof with auto. constructor. replace (@integrate g) with (@integrate f) by reflexivity. intros. apply integral_additive. replace (@integrate g) with (@integrate f) by reflexivity. intros. apply integral_bounded_prim... intros. assert (msp_eq (f x) (g x)). { apply H. reflexivity. } rewrite H3... replace (@integrate g) with (@integrate f) by reflexivity. apply integral_wd... 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