proposition: Lemma DestructCSUCposPoint : { l : CRcarrier R | (forall k:nat, CRsum (fun n => fn n l) k <= g l) /\ x (CSUCposPointApproxSequence 0) <= l /\ l <= y (CSUCposPointApproxSequence 0) }.
proof: Proof. pose proof CSUCIcontinuous. pose proof CSUCposPointApproxLimitNested. destruct CSUCposPointApproxSequenceCauchy as [l lcv]. exists l. split. exact H. apply H0. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets