proposition: Lemma Rser_equiv_cv : forall (Un Vn : nat -> R), (forall n : nat, 0 <= Un n) -> (forall n : nat, 0 <= Vn n) -> Un ~ Vn -> {lv | Rser_cv Vn lv} -> {lu | Rser_cv Un lu}.
proof: Proof. intros Un Vn Un_pos Vn_pos Heq Hlv. apply Rseq_equiv_sym in Heq. assert ({luv | Rser_cv (fun n => Rabs (Vn n - Un n)) luv}) as Hluv. apply Rser_little_O_cv with Vn. unfold Rseq_little_O. intros eps Heps. destruct (Heq eps Heps) as [N HN]; exists N. intro n; apply HN. destruct Hlv as [lv Hlv]. exists lv; apply Rser_cv_ext with Vn. intros n; unfold Rseq_abs; rewrite Rabs_right; auto with real. assumption. destruct Hlv as [lv Hlv]. destruct Hluv as [luv Hluv]. apply Rser_pos_bound_cv with (lv + luv)%R. apply Un_pos. intro n. apply Rle_trans with (sum_f_R0 Vn n + sum_f_R0 (fun n : nat => Rabs (Vn n - Un n)) n)%R. apply Rle_trans with (sum_f_R0 (fun n0 : nat => Vn n0 + Rabs (Vn n0 - Un n0)) n)%R. apply sum_Rle. intros n0 Hn0. rewrite <- ( Rabs_pos_eq) with (Vn n0). rewrite Rabs_pos_eq at 2. rewrite <- Rabs_pos_eq with (Un n0). rewrite Rabs_pos_eq at 2. rewrite <- Rabs_Ropp. rewrite <- Rabs_Ropp with (Vn n0). replace (- Un n0)%R with (- Vn n0 + (Vn n0 - Un n0))%R by ring. apply Rabs_triang. apply Un_pos . apply Un_pos. apply Vn_pos. apply Vn_pos. rewrite plus_sum. apply Rplus_le_compat_l. apply Rle_refl. apply Rplus_le_compat; [ | ]; apply growing_ineq. apply Rser_pos_growing. apply Vn_pos. apply Hlv. apply Rser_pos_growing. intro k; apply Rabs_pos. apply Hluv. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq