proposition: Lemma ln_minus_taylor : forall x, Rabs x < 1 -> Pser Un x (ln (1 - x)).
proof: Proof. intros x Hx. rewrite <- ln_minus_taylor_sum; [|assumption]. apply weaksum_r_sums; assumption. 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