proposition: Lemma ratio_test_div : {N : nat | {c : IR | [1] [<=] c | forall n, N <= n -> c[*]AbsIR (x n) [<] AbsIR (x (S n))}} -> divergent x.
proof: Proof. intros H. elim H; clear H; intros N H. elim H; clear H; intros c Hc Hn. apply divergent_crit. exists (AbsIR (x (S N))). apply leEq_less_trans with (c[*]AbsIR (x N)). astepl (c[*][0]); apply mult_resp_leEq_lft. apply AbsIR_nonneg. apply less_leEq; eapply less_leEq_trans; [ apply pos_one | assumption ]. apply Hn; auto with arith. cut (forall n : nat, S N <= n -> {m : nat | n <= m /\ AbsIR (x (S N)) [<=] AbsIR (x m)}). intro H. clear Hn. intro n. cut (S N <= Nat.max (S N) n); [ intro | apply Nat.le_max_l ]. elim (H _ H0); intros m Hm; elim Hm; clear H Hm; intros Hm H; exists m. apply Nat.le_trans with (Nat.max (S N) n); auto with arith. assumption. intros; exists n. split. auto. induction n as [| n Hrecn]. inversion H. clear Hrecn; induction n as [| n Hrecn]. inversion H. rewrite <- H1; apply eq_imp_leEq; algebra. inversion H1. elim (le_lt_eq_dec _ _ H); intro. apply leEq_transitive with (AbsIR (x (S n))). apply Hrecn; auto with arith. apply less_leEq; apply leEq_less_trans with (c[*]AbsIR (x (S n))). astepl ([1][*]AbsIR (x (S n))); apply mult_resp_leEq_rht. assumption. apply AbsIR_nonneg. apply Hn; auto with arith. rewrite b; apply eq_imp_leEq; algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)