proposition: Lemma Pser_add : forall (An Bn : nat -> C) (z : C) (N : nat), sum_f_C0 (gt_pser (fun n => An n + Bn n) z) N = sum_f_C0 (gt_pser An z) N + sum_f_C0 (gt_pser Bn z) N.
proof: Proof. intros An Bn x N ; induction N. simpl ; unfold gt_pser, Cseq_mult ; field. assert (Hrew : forall a b c d e, c = d + e -> a + b + c = a + d + (b + e)). intros ; subst ; field. simpl ; rewrite IHN ; apply Hrew. unfold gt_pser, Cseq_mult ; field. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia