proposition: Lemma divergent_crit : {r : IR | [0] [<] r | forall n, {m : nat | n <= m | r [<=] AbsIR (x m)}} -> divergent x.
proof: Proof. intro H. elim H; clear H; intros r Hr H. exists r. assumption. intro. elim (H k); clear H; intros m Hm Hrm. exists (S m). exists m. split. auto. split. assumption. eapply leEq_wdr. apply Hrm. apply AbsIR_wd. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. apply seq_part_sum_n; auto with arith. apply Sum_one. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)