proposition: Lemma sum_f_C0_opp_compat : forall (f : nat -> C) (N : nat), sum_f_C0 (fun n => - f n) N = - sum_f_C0 f N.
proof: Proof. induction N. reflexivity. simpl ; rewrite IHN ; ring. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia