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