proposition: Lemma Cpser_unique_extentionality : forall (An Bn : nat -> C) (x l1 l2 : C), (forall n, An n = Bn n) -> Cpser An x l1 -> Cpser Bn x l2 -> l1 = l2.
proof: Proof. intros An Bn x l1 l2 An_eq_Bn Hl1 Hl2. assert (T1 := Pser_Cseqcv_link _ _ _ Hl1) ; assert (T2 := Pser_Cseqcv_link _ _ _ Hl2). assert (T3 : forall (n : nat), sum_f_C0 (fun n => (gt_pser An x) n) n = sum_f_C0 (fun n => (gt_pser Bn x) n) n). intro n ; apply (sum_f_C0_eq_seq) ; intros ; unfold gt_pser, Cseq_mult ; rewrite An_eq_Bn ; reflexivity. assert (T4 := Cseq_cv_eq_compat _ _ _ T3 T1). 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