proposition: Lemma Rser_partial_equiv_compat : forall (Un : nat -> R), Un ~ Vn -> (sum_f_R0 Un) ~ (sum_f_R0 Vn).
proof: Proof. intros Un Heq. apply Rseq_equiv_sym. apply Rseq_equiv_sym in Heq. assert((sum_f_R0 (Vn -Un)) = o(sum_f_R0 Vn)). apply (Rser_partial_little_O_compat (Vn - Un) Heq ). intros eps Heps. destruct (H eps Heps) as [N HN]. exists N; intros n Hn. unfold Rseq_minus. rewrite <- minus_sum. apply HN; apply Hn. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq