proposition: Lemma Rser_little_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 Hcv. apply (Rser_big_O_cv Un Vn); [|assumption]. apply Rseq_little_O_big_O_incl; 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