proposition: Lemma Rser_big_O_cv : forall (Un Vn : nat -> R), Un = O(Vn) -> {lv | Rser_abs_cv Vn lv} -> {lu | Rser_abs_cv Un lu}.
proof: Proof. intros Un Vn HO Hlv. apply Rser_big_O_cv_weak with (|Vn|); intros; apply Rabs_pos || auto. destruct HO as [M [HM [N HN]]]; exists M. split; auto. exists N; intros. unfold Rseq_abs; rewrite Rabs_Rabsolu; auto. rewrite Rabs_Rabsolu; apply HN; assumption. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq