proposition: Lemma finite_cv_radius_pos : forall An r, finite_cv_radius An r -> 0 <= r.
proof: Proof. intros An r [_ Hf]. destruct(Rle_lt_dec 0 r). trivial. destruct (Hf R0). trivial. apply Cv_radius_weak_0. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia