proposition: Lemma Rser_equiv_cv_infty : forall (Un Vn : nat -> R), (forall n : nat, 0 <= Un n) -> (forall n : nat, 0 <= Vn n) -> Un ~ Vn -> Rser_cv_pos_infty Vn -> Rser_cv_pos_infty Un.
proof: Proof. intros Un Vn Un_pos Vn_pos Heq Hv. case (Rser_pos_cv_dec Un Un_pos NNPP classic); intro Hcase. apply Rseq_growing_constructive_limit in Hcase. apply (Rser_equiv_cv Vn Un) in Hcase. assert ((exists l, Rser_cv Vn l)/\ Rser_cv_pos_infty Vn). split. destruct Hcase as [ l Hl]. exists l; apply Hl. apply Hv. elim Rseq_cv_not_infty with (sum_f_R0 Vn). apply H. apply Vn_pos. apply Un_pos. apply Rseq_equiv_sym. apply Heq. apply Rser_pos_growing. apply Un_pos. apply Hcase. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq