proposition: Lemma UC_integral_extend_nonneg : 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, 0 <= (f x)) -> 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). exact H0. } rewrite (UC_integral_chasles c a d f modF fCont H H2). rewrite (UC_integral_chasles a b d f modF fCont leab H0). apply (CRplus_le_reg_l (- UC_integral f a b modF fCont leab)). apply CRplus_le_compat_l. rewrite CRplus_comm. rewrite <- (CRplus_0_r (UC_integral f a b modF fCont leab)). do 2 rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. rewrite <- (CRplus_0_r 0). apply CRplus_le_compat. apply UC_integral_pos. intros. apply H1. apply UC_integral_pos. intros. apply H1. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont