proposition: Lemma abs_imp_conv : fun_series_abs_convergent _ _ Hab f -> fun_series_convergent _ _ Hab f.
proof: Proof. intro H. apply fun_comparison with (fun n : nat => FAbs (f n)). apply H. intros; apply eq_imp_leEq; apply eq_symmetric_unfolded; apply FAbs_char. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series