proposition: Lemma diff_series_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 R un l) (l <= s + CRabs R (un O)) }.
proof: Proof. intros. destruct (series_cv_maj (fun n:nat => match n with | O => un O | S p => un n - un p end) (fun n:nat => match n with | O => CRabs R (un O) | S p => vn p end) (s + CRabs R (un O))) as [l lcv]. - intro n. destruct n. apply CRle_refl. apply H. - intro p. specialize (H0 p) as [n ncv]. exists (S n). intros. destruct i. exfalso; inversion H0. rewrite decomp_sum. simpl. unfold CRminus. rewrite CRplus_comm, CRopp_plus_distr, CRplus_assoc. rewrite <- (CRplus_assoc (-CRabs R (un O))), CRplus_opp_l, CRplus_0_l. rewrite CRplus_comm. apply ncv. apply le_S_n, H0. apply le_n_S, Nat.le_0_l. - exists l. split. 2: exact (snd lcv). apply (CR_cv_eq _ (CRsum (fun n : nat => match n with | 0%nat => un 0%nat | S p => un n - un p end))). + induction n. reflexivity. simpl. rewrite IHn. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. + exact (fst lcv). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia