proposition: Lemma Pser_minus : forall (An Bn : nat -> C) (x : C) (N : nat), sum_f_C0 (gt_pser (fun n => An n - Bn n) x) N = sum_f_C0 (gt_pser An x) N - sum_f_C0 (gt_pser Bn x) 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