proposition: Lemma Pser_unique : forall (An : nat -> C) (x l1 l2 : C), Cpser An x l1 -> Cpser An x l2 -> l1 = l2.
proof: Proof. intros An x l1 l2 Hl1 Hl2. assert (T1 := Pser_Cseqcv_link _ _ _ Hl1) ; assert (T2 := Pser_Cseqcv_link _ _ _ Hl2) ; eapply Cseq_cv_unique ; eassumption. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia