proposition: Lemma ratio_test_conv : {N : nat | {c : IR | c [<] [1] | [0] [<=] c /\ (forall n, N <= n -> AbsIR (x (S n)) [<=] c[*]AbsIR (x n))}} -> convergent x.
proof: Proof. intro H. elim H; clear H; intros N H. elim H; clear H; intros c Hc1 H. elim H; clear H; intros H0c H. cut (forall n : nat, N <= n -> AbsIR (x n) [<=] AbsIR (x N) [*]c[^] (n - N)). intro. apply str_comparison with (fun n : nat => AbsIR (x N) [*]c[^] (n - N)). 2: exists N; assumption. apply conv_series_mult_scal with (x := fun n : nat => c[^] (n - N)). apply join_series with (power_series c). apply power_series_conv. apply AbsIR_less. assumption. apply less_leEq_trans with [0]. rstepr ([--][0]:IR). apply inv_resp_less. apply pos_one. assumption. exists N. exists 0. intro. rewrite Nat.add_sub. algebra. simple induction n. intro. cut (N = 0); [ intro | auto with arith ]. rewrite H1. apply eq_imp_leEq. simpl in |- *; algebra. clear n; intros. cut ({N < S n} + {N = S n}). 2: apply le_lt_eq_dec; assumption. intro; inversion_clear H2. apply leEq_transitive with (c[*]AbsIR (x n)). apply H; auto with arith. rewrite Nat.sub_succ_l. astepr (AbsIR (x N) [*] (c[*]c[^] (n - N))). rstepr (c[*] (AbsIR (x N) [*]c[^] (n - N))). apply mult_resp_leEq_lft. apply H0; auto with arith. assumption. auto with arith. rewrite H3. rewrite Nat.sub_diag. apply eq_imp_leEq. simpl in |- *; algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)