proposition: Lemma Rseq_ln_cv : Rseq_cv_pos_infty (fun n => ln (INR n)).
proof: Proof. intro m. destruct (Rseq_poly_cv 1) with (M := Rabs m) as [N HN]; [lia|]. destruct (IZN(up (exp (INR N)))) as [N1 HN1]. apply le_IZR; simpl. apply Rle_trans with (exp (INR N)). left; apply exp_pos. left; eapply (proj1 (archimed _)). exists N1. intros n Hn. apply Rle_lt_trans with (Rabs m). apply RRle_abs. apply Rlt_le_trans with (INR N). replace (INR N) with (INR N ^ 1) by field. apply (HN _ (Nat.le_refl _)). rewrite <- ln_exp with (INR N). left; apply ln_increasing. apply exp_pos. apply Rlt_le_trans with (IZR (Z_of_nat N1)). rewrite <- HN1. apply (proj1(archimed _)). rewrite <- INR_IZR_INZ; apply le_INR; apply Hn. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra