proposition: Lemma Un_cv : {l | Rseq_cv Un l & 0 < l}.
proof: Proof. assert (Hcv : {l | Rseq_cv (fun n => ln (Un n)) l}). destruct Rser_cv_Vn as [l Hl]. exists (l + ln (Un 1)). eapply Rseq_cv_asymptotic. intros Xn HX; pattern Xn; apply HX. exists 1%nat; intros eps Heps. destruct (Hl eps Heps) as [N HN]. exists N; intros n Hn. unfold R_dist, Rseq_shifts. replace (1 + n)%nat with (S n) by lia. replace (ln (Un (S n)) - (l + (ln (Un 1)))) with (ln (Un (S n)) - ln (Un 1) - l) by ring. rewrite <- Vn_ser_eq. apply HN; assumption. destruct Hcv as [l Hl]. exists (exp l). eapply Rseq_cv_asymptotic. intros Xn HX; pattern Xn; apply HX. exists 1%nat. eapply Rseq_cv_eq_compat with (fun n => exp (ln (Un (S n)))). intros n; rewrite exp_ln. replace (S n) with (1 + n)%nat by lia; reflexivity. apply Un_pos; lia. apply Rseq_cv_continuity_compat. intros eps Heps. destruct (Hl eps Heps) as [N HN]. exists N; intros n Hn. apply HN; lia. apply derivable_continuous_pt. apply derivable_exp. apply exp_pos. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis