proposition: Lemma UC_integral_extens : forall {R : ConstructiveReals} f g a b (modF : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (modG : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f modF) (gCont : UniformCont g modG) (leab leabb : a <= b), (forall x, (a <= x /\ x <= b) -> f x == g x) -> UC_integral f a b modF fCont leab == UC_integral g a b modG gCont leabb.
proof: Proof. intros. split; apply UC_integral_nonneg. intros. rewrite H. apply CRle_refl. exact H0. intros. rewrite H. apply CRle_refl. exact H0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont