proposition: Lemma fun_str_comparison_IR : forall g : nat -> PartIR, fun_series_convergent_IR J g -> {k : nat | forall n, k <= n -> forall x, J x -> forall Hx Hx', AbsIR (f n x Hx) [<=] g n x Hx'} -> fun_series_convergent_IR J f.
proof: Proof. intros g H H0 a b Hab H1. apply fun_str_comparison with g. intro; apply included_imp_Continuous with J; auto. auto. elim H0; clear H0; intros k Hk. exists k; intros. apply Hk; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions