proposition: Lemma fun_ratio_test_conv_IR : {N : nat | {c : IR | c [<] [1] | [0] [<=] c /\ (forall x, J x -> forall n, N <= n -> forall Hx Hx', AbsIR (f (S n) x Hx') [<=] c[*]AbsIR (f n x Hx))}} -> fun_series_convergent_IR J f.
proof: Proof. intro H. red in |- *; intros. apply fun_ratio_test_conv. intro; apply included_imp_Continuous with J; auto. elim H; intros N HN. elim HN; clear H HN; intros c Hc H. inversion_clear H. exists N; exists c; repeat split; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions