proposition: Lemma series_cv_remainder_cv : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l eps : CRcarrier R), series_cv un l -> 0 < eps -> { k : nat & forall i:nat, le k i -> series_cv_lim_lt (fun n => un (n + i)%nat) eps }.
proof: Proof. intros. destruct (Un_cv_nat_real (CRsum un) l H eps H0) as [k kmaj]. exists (S k). intros. pose proof (series_cv_shift' un l i H). destruct i. exfalso; inversion H1. exists (l - CRsum un i). split. exact H2. apply le_S_n in H1. specialize (kmaj i H1). rewrite CRabs_minus_sym in kmaj. exact (CRle_lt_trans _ _ _ (CRle_abs _) kmaj). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions