proposition: Lemma sum_f_C0_triang : 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 ; simpl. intuition (auto with real). apply Rle_trans with (Cnorm (sum_f_C0 f N) + Cnorm (f (S N)))%R. apply Cnorm_triang. apply Rplus_le_compat_r ; assumption. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia