proposition: Lemma abs_imp_conv_IR : fun_series_abs_convergent_IR J f -> fun_series_convergent_IR J f.
proof: Proof. intro H. apply fun_comparison_IR with (fun n => FAbs (f n)). apply H. intros; apply eq_imp_leEq; apply eq_symmetric_unfolded; apply FAbs_char. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions