proposition: Lemma Cser_cv_eq_compat : forall Un Vn l, (forall j, Un j = Vn j) -> Cser_cv Un l -> Cser_cv Vn l.
proof: Proof. intros Un Vn l H HC. apply Cseq_cv_eq_compat with (sum_f_C0 Un). intro; apply Csum_eq_compat_weak; apply H. apply HC. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Lia Lra Complex Csequence_facts Cseries