proposition: Lemma Rseries_CV_comp : forall An Bn:nat -> R, (forall n:nat, 0 <= An n <= Bn n) -> { l:R | Un_cv (fun N:nat => sum_f_R0 Bn N) l } -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
proof: Proof. intros An Bn H X; apply cv_cauchy_2. assert (H0 := cv_cauchy_1 _ X). unfold Cauchy_crit_series; unfold Cauchy_crit. intros; elim (H0 eps H1); intros. exists x; intros. cut (Rdist (sum_f_R0 An n) (sum_f_R0 An m) <= Rdist (sum_f_R0 Bn n) (sum_f_R0 Bn m)). { intro; apply Rle_lt_trans with (Rdist (sum_f_R0 Bn n) (sum_f_R0 Bn m)). - assumption. - apply H2; assumption. } destruct (lt_eq_lt_dec n m) as [[| -> ]|]. - rewrite (tech2 An n m); [ idtac | assumption ]. rewrite (tech2 Bn n m); [ idtac | assumption ]. unfold Rdist; unfold Rminus; do 2 rewrite Ropp_plus_distr; do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r; do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right. + apply sum_Rle; intros. elim (H (S n + n0)%nat); intros H7 H8. apply H8. + apply Rle_ge; apply cond_pos_sum; intro. elim (H (S n + n0)%nat); intros. apply Rle_trans with (An (S n + n0)%nat); assumption. + apply Rle_ge; apply cond_pos_sum; intro. elim (H (S n + n0)%nat); intros; assumption. - unfold Rdist; unfold Rminus; do 2 rewrite Rplus_opp_r; rewrite Rabs_R0; right; reflexivity. - rewrite (tech2 An m n); [ idtac | assumption ]. rewrite (tech2 Bn m n); [ idtac | assumption ]. unfold Rdist; unfold Rminus; do 2 rewrite Rplus_assoc; rewrite (Rplus_comm (sum_f_R0 An m)); rewrite (Rplus_comm (sum_f_R0 Bn m)); do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l; do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right. + apply sum_Rle; intros. elim (H (S m + n0)%nat); intros H7 H8; apply H8. + apply Rle_ge; apply cond_pos_sum; intro. elim (H (S m + n0)%nat); intros. apply Rle_trans with (An (S m + n0)%nat); assumption. + apply Rle_ge. apply cond_pos_sum; intro. elim (H (S m + n0)%nat); intros; assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp Rcomplete PartSum AltSeries Binomial Rsigma Rprod Cauchy_prod Alembert Lra