proposition: Lemma infinite_sum_truncate_below : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (s : CRcarrier R) (N : nat), series_cv u s -> series_cv (fun n : nat => if le_dec n N then 0 else u n) (s - CRsum u N).
proof: Proof. intros. apply (series_cv_eq (fun n : nat => u n + (if le_dec n N then (-u n) else 0))). intros. destruct (le_dec n N). rewrite CRplus_opp_r. reflexivity. rewrite CRplus_0_r. reflexivity. apply series_cv_plus. assumption. intros n. exists N. intros. rewrite sum_truncate_above. rewrite <- (CRsum_eq (fun n0 : nat => u n0 * (CRopp R 1))). rewrite sum_scale, CRmult_comm. rewrite <- (CRopp_mult_distr_l 1). unfold CRminus. rewrite <- CRopp_plus_distr. rewrite CRabs_opp. rewrite CRmult_1_l. rewrite CRplus_opp_r. rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. intros. rewrite <- CRopp_mult_distr_r, CRmult_1_r. reflexivity. assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase