proposition: Lemma series_cv_remainder_maj : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (s eps : CRcarrier R) (N : nat), series_cv u s -> 0 < eps -> (forall n:nat, 0 <= u n) -> CRabs R (CRsum u N - s) <= eps -> forall n:nat, CRsum (fun k=> u (N + S k)%nat) n <= eps.
proof: Proof. intros. pose proof (sum_assoc u N n). rewrite <- (CRsum_eq (fun k : nat => u (S N + k)%nat)). - apply (CRplus_le_reg_l (CRsum u N)). rewrite <- H3. apply (CRle_trans _ s). + apply growing_ineq. 2: apply H. intro k. simpl. rewrite <- CRplus_0_r, CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. apply H1. + rewrite CRabs_minus_sym in H2. rewrite CRplus_comm. apply (CRplus_le_reg_r (-CRsum u N)). rewrite CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_r. apply (CRle_trans _ (CRabs R (s - CRsum u N))). * apply CRle_abs. * assumption. - intros. rewrite Nat.add_succ_r. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits