proposition: Lemma fun_comparison : forall g, fun_series_convergent _ _ Hab g -> (forall n x, I x -> forall Hx Hx', AbsIR (f n x Hx) [<=] g n x Hx') -> fun_series_convergent _ _ Hab f.
proof: Proof. intros g H H0. apply fun_str_comparison with g; auto. exists 0; intros; apply H0; auto. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series