proposition: Lemma splitInfiniteSumMaj : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a s : CRcarrier R), series_cv u s -> a < s -> { N : nat | CRltProp R (a + s - CRsum u N) (CRsum u N) }.
proof: Proof. intros. destruct (Un_cv_nat_real _ s H ((s - a) * CR_of_Q R (1 # 2))) as [N H1]. + apply CRmult_lt_0_compat. rewrite <- (CRplus_opp_r a). apply CRplus_lt_compat_r. exact H0. apply CR_of_Q_lt. reflexivity. + exists N. specialize (H1 N (Nat.le_refl N)). rewrite CRabs_minus_sym in H1. apply (CRle_lt_trans (s - CRsum u N)) in H1. apply (CRmult_lt_compat_r (CR_of_Q R 2)) in H1. rewrite CRmult_assoc in H1. rewrite <- CR_of_Q_mult in H1. setoid_replace ((1 # 2) * 2)%Q with 1%Q in H1. 2: reflexivity. rewrite CRmult_1_r in H1. assert ((s - CRsum u N) * CR_of_Q R 2 == s + s - CRsum u N -CRsum u N). { rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. unfold CRminus. do 3 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm, CRplus_assoc. reflexivity. } rewrite H2 in H1. unfold CRminus in H1. apply (CRplus_lt_compat_l _ (-s)) in H1. rewrite <- CRplus_assoc, <- CRplus_assoc in H1. rewrite <- CRplus_assoc in H1. rewrite CRplus_opp_l in H1. rewrite CRplus_0_l in H1. rewrite <- CRplus_assoc in H1. rewrite CRplus_opp_l in H1. rewrite CRplus_0_l in H1. apply (CRplus_lt_compat_l _ a) in H1. rewrite CRplus_opp_r in H1. apply (CRplus_lt_compat_r (CRsum u N)) in H1. rewrite CRplus_assoc in H1. rewrite CRplus_assoc in H1. rewrite CRplus_opp_l in H1. rewrite CRplus_0_r in H1. rewrite CRplus_0_l in H1. rewrite <- CRplus_assoc in H1. apply CRltForget. assumption. apply CR_of_Q_lt. reflexivity. apply CRle_abs. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase