proposition: Lemma fun_series_conv_imp_conv_IR : fun_series_convergent_IR -> forall x, J x -> forall Hx, convergent (fun n : nat => f n x (Hx n)).
proof: Proof. intros H x H0 Hx. apply fun_series_conv_imp_conv with (Hab := leEq_reflexive _ x). apply H. fold (compact_single x) in |- *; apply compact_single_iprop; auto. apply compact_single_prop. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions