proposition: Lemma UC_integral_extend_zero : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (modF : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (a b c d : CRcarrier R) (fCont : UniformCont f modF) (leab : a <= b) (lecd : c <= d), c <= a -> b <= d -> (forall x : CRcarrier R, (c <= x /\ x <= a) -> f x == 0) -> (forall x : CRcarrier R, (b <= x /\ x <= d) -> f x == 0) -> UC_integral f a b modF fCont leab == UC_integral f c d modF fCont lecd.
proof: Proof. intros. assert (a <= d). { apply (CRle_trans _ _ _ leab H0). } rewrite (UC_integral_chasles c a d f modF fCont H H3). rewrite (UC_integral_chasles a b d f modF fCont leab H0). rewrite (UC_integral_zero f c a). rewrite (UC_integral_zero f b d). rewrite CRplus_0_l, CRplus_0_r. reflexivity. exact H2. exact H1. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont