proposition: Lemma fun_comparison_IR : forall g : nat -> PartIR, fun_series_convergent_IR J g -> (forall n 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. apply fun_str_comparison_IR with g; auto. exists 0; intros; apply H0; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions