proposition: Lemma Cser_cv_re_compat : forall Un l, Cser_cv Un l -> Rser_cv (fun n : nat => Cre (Un n)) (Cre l).
proof: Proof. intros Un l HC. apply Rseq_cv_eq_compat with (fun n => Cre (sum_f_C0 Un n)). intro; rewrite sum_f_C0_Cre_compat; trivial. apply Cseq_cv_re_compat. apply HC. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Lia Lra Complex Csequence_facts Cseries