proposition: Lemma sum_f_C0_mult : forall (z : C) (f : nat -> C) (N : nat), z * (sum_f_C0 (fun n => f n) N) = sum_f_C0 (fun n => z* (f n)) N .
proof: Proof. intros z f0 n. induction n. reflexivity. simpl ; rewrite <- IHn ; ring. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia