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