proposition: Lemma CR_cv_maj : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (s : CRcarrier R), (forall n:nat, CRabs R (un (S n) - un n) <= vn n) -> series_cv vn s -> { l : CRcarrier R & prod (CR_cv _ un l) (l <= s + un O) }.
proof: Proof. intros. destruct (series_cv_maj (fun n => un (S n) - un n) vn s H H0) as [l [lcv lmaj]]. apply (CR_cv_eq (fun n => un (S n) - un O)) in lcv. - exists (l + un O). split. apply (CR_cv_shift _ 1). apply (CR_cv_eq _ (fun n => un (S n) - un O + un O)). intros. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite Nat.add_comm. reflexivity. apply CR_cv_plus. exact lcv. apply CR_cv_const. unfold CRminus. apply CRplus_le_compat_r. exact lmaj. - induction n. reflexivity. simpl. rewrite IHn. clear IHn. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile