proposition: Lemma ln_minus_cv_radius : Cv_radius_weak Un 1.
proof: Proof. exists 1; intros m [n Hn]; subst m. unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult. rewrite pow1; rewrite Rmult_1_r. unfold Un; destruct n. rewrite Rabs_R0; apply Rle_0_1. assert (Hle : 1 <= INR (S n)). rewrite S_INR. pattern 1 at 1; rewrite <- Rplus_0_l. apply Rplus_le_compat_r. apply pos_INR. rewrite Rabs_Ropp. rewrite Rabs_Rinv; [|intros Hc; lra]. rewrite Rabs_right; [|lra]. apply (Rmult_le_reg_l (INR (S n))); [lra|]. rewrite Rinv_r; [lra|intros Hc; lra]. Qed.
imports: Reals MyReals Rsequence_def Rsequence_facts Rsequence_sums_facts Rseries_def Rpser_def Rpser_sums Rpser_sums_facts Rpser_derivative Rpser_radius_facts Rpser_taylor Lra Rintegral Rseries_facts Rseries_RiemannInt Rsequence_subsequence Rtactic