proposition: Lemma Cser_cv_unique : forall Un l1 l2, Cser_cv Un l1 -> Cser_cv Un l2 -> l1 = l2.
proof: Proof. intros Un l1 l2 H H'. apply Cseq_cv_unique with (sum_f_C0 Un); auto. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Lia Lra Complex Csequence_facts Cseries