proposition: Lemma finite_cv_radius_weakening : forall An 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_le_compat with (Rabs x). rewrite Rabs_Rabsolu ; right ; reflexivity. apply H_sup ; split ; [apply Rabs_pos | assumption]. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia