proposition: Lemma Rpser_abel : forall (An : nat -> R) (r : R), Cv_radius_weak An r -> forall x, Rabs x < r -> {l | Rpser An x l}.
proof: Proof. intros An r Rho x x_ub. apply R_complete ; apply Cauchy_crit_Rseq_pps with r ; assumption. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics