proposition: Lemma sum_f_C0_Cnorm_compat : forall (f : nat -> C) (N : nat), Cnorm (sum_f_C0 f N) <= sum_f_R0 (fun n => Cnorm (f n)) N.
proof: Proof. induction N. right. reflexivity. simpl. eapply Rle_trans. apply Cnorm_triang. apply Rplus_le_compat. apply IHN. right. reflexivity. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia