proposition: Lemma Pser_Cseqcv_link : forall (An : nat -> C) (x l : C), Cpser An x l -> Cseq_cv (fun N : nat => sum_f_C0 (gt_pser An x) N) l.
proof: Proof. intros An x l H ; apply H. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia