proposition: Lemma CSUCIcontinuous : let (l,_) := CSUCposPointApproxSequenceCauchy in forall k:nat, CRsum (fun n => fn n l) k <= g l.
proof: Proof. pose proof CSUCposPointApproxLimitNested. destruct CSUCposPointApproxSequenceCauchy as [l lcv]. intro k. intro abs. destruct (UC_sum (fun n x => fn n x) fnMod fnCont k) as [modS contS]. destruct (EnlargePointMajoration g _ l gMod modS (fst gCSUC) contS abs) as [eta [etaPos etaMaj]]. destruct (CRup_nat (CRinv R eta (inr etaPos))) as [p pmaj]. assert (0 < @INR R p) as qpPos. { apply (CRlt_trans _ (CRinv R eta (inr etaPos))). apply CRinv_0_lt_compat. exact etaPos. exact pmaj. } assert (0 < p)%nat. { unfold INR in qpPos. destruct p. 2: apply le_n_S, Nat.le_0_l. exfalso. contradict qpPos. apply (CRle_trans _ (CR_of_Q R 0)). apply CR_of_Q_le. discriminate. apply CRle_refl. } destruct (CSUCposPointApproxSequenceCvZero (Pos.of_nat p)) as [i imaj]. specialize (imaj i (Nat.le_refl i)). specialize (H i). destruct (CSUCposPointApproxSequence i); unfold x,y in imaj. destruct lambdaInfiniteMaj0. simpl in H. assert (CRsum (fun j : nat => UC_integral (fn j) x0 y0 (fnMod j) (fnCont j) lexy0) k < UC_integral g x0 y0 gMod (fst gCSUC) lexy0). { apply (CRle_lt_trans _ x1). 2: apply p0. apply growing_ineq. 2: apply p0. intros n. rewrite <- (CRplus_0_r (CRsum (fun j : nat => UC_integral (fn j) x0 y0 (fnMod j) (fnCont j) lexy0) n)). apply CRplus_le_compat_l. apply UC_integral_pos. intros. apply fnPos. } assert (forall x y : CRcarrier R, x < y -> ~(y<=x)) as CReal_lt_not_le. { intros. intro abs1. contradiction. } apply (CReal_lt_not_le _ _ H1). destruct (UC_sum fn fnMod fnCont k) as [modSk c]. rewrite <- (UC_integral_sum fn _ _ k _ _ fnCont c). apply UC_integral_nonneg. intros. apply CRlt_asym, etaMaj. rewrite CRabs_right in imaj. apply (CRle_lt_trans _ (y0- x0)). apply Rsmaller_interval. apply H2. apply H2. apply H. apply H. apply (CRlt_trans _ (CR_of_Q R (1#Pos.of_nat p))). unfold CRminus. exact imaj. 2: rewrite <- (CRplus_opp_r x0); apply CRplus_le_compat_r, lexy0. apply (CRmult_lt_compat_l eta) in pmaj. rewrite CRinv_r in pmaj. 2: exact etaPos. apply (CRmult_lt_reg_r (INR p)). exact qpPos. apply (CRle_lt_trans _ 1). 2: exact pmaj. unfold INR. rewrite <- CR_of_Q_mult. apply CR_of_Q_le. unfold Qmult, Qle, Qden, Qnum. rewrite Z.mul_1_l, Z.mul_1_l, Pos.mul_1_r. rewrite Z.mul_1_r. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. apply Z.le_refl. intro abs1. subst p. inversion H0. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets