proposition: Lemma Cser_cv_re_im_compat : forall Un l, Rser_cv (fun n => Cre (Un n)) (Cre l) -> Rser_cv (fun n => Cim (Un n)) (Cim l) -> Cser_cv Un l.
proof: Proof. intros Un l HCre HCim. apply Cseq_cv_re_im_compat. apply Rseq_cv_eq_compat with (sum_f_R0 (fun n => Cre (Un n))). intro; rewrite <- sum_f_C0_Cre_compat; trivial. apply HCre. apply Rseq_cv_eq_compat with (sum_f_R0 (fun n => Cim (Un n))). intro; rewrite <- sum_f_C0_Cim_compat; trivial. apply HCim. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Lia Lra Complex Csequence_facts Cseries