fact: Variable (R : ConstructiveReals) (g : CRcarrier R -> CRcarrier R) (fn : nat -> CRcarrier R -> CRcarrier R) (fnPos : forall (k:nat) (x:CRcarrier R), 0 <= fn k x) (fnMod : nat -> forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fnCont : forall n:nat, UniformCont (fn n) (fnMod n)) (gMod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (a b : CRcarrier R) (leab : a <= b) (gCSUC : CSUC g a b gMod) (majInt : series_cv_lim_lt (fun k : nat => UC_integral (fn k) a b (fnMod k) (fnCont k) leab) (UC_integral g a b gMod (fst gCSUC) leab)).
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets