proposition: Lemma ln_plus_taylor_sum : forall x, Rabs x < 1 -> sum x = (ln (1 + x)).
proof: Proof. intros x Hx. assert (Hmx : Rabs (- x) < 1). rewrite Rabs_Ropp; assumption. replace (1 + x) with (1 - (- x)) by ring. eapply trans_eq; [|apply ln_minus_taylor_sum; assumption]. eapply Rseq_cv_unique. apply weaksum_r_sums; assumption. eapply Rseq_cv_eq_compat; [|apply weaksum_r_sums; assumption]. intros n; apply sum_eq; intros i Hi; unfold Un. unfold gt_pser. unfold Rseq_mult. destruct i; [field|]. replace (- x) with (- 1 * x) by ring. rewrite Rpow_mult_distr. repeat rewrite <- tech_pow_Rmult; field. auto with real. 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