proposition: Lemma PrependSeqSeries : forall {R : ConstructiveReals} (x : CRcarrier R) (un : nat -> CRcarrier R) (l : CRcarrier R), series_cv un l -> series_cv (PrependSeq x un) (x + l).
proof: Proof. intros. intros n. specialize (H n) as [p pmaj]. exists (S p). intros. destruct i. exfalso; inversion H. apply le_S_n in H. rewrite decomp_sum. simpl. setoid_replace (x + CRsum (fun i0 : nat => un i0) i - (x + l)) with (CRsum (fun i0 : nat => un i0) i - l). apply pmaj. exact H. 2: apply le_n_S, Nat.le_0_l. unfold CRminus. rewrite (CRplus_comm x). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions