proposition: Lemma conv_fun_const_series_IR : forall x : nat -> IR, convergent x -> fun_series_convergent_IR J (fun n => [-C-] (x n)).
proof: Proof. intros. red in |- *; intros. apply conv_fun_const_series; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions