proposition: Lemma finite_cv_radius_weakening : forall (An : Rseq) (r : R), finite_cv_radius An r -> forall x, Rabs x < r -> Cv_radius_weak An x.
proof: Proof. intros An r [H_sup _] x Hx ; apply Cv_radius_weak_Rabs ; apply H_sup ; split ; [apply Rabs_pos | assumption]. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR