proposition: Lemma finite_cv_radius_pos : forall (An : Rseq) (r : R), finite_cv_radius An r -> 0 <= r.
proof: Proof. intros An r [_ Hf] ; destruct(Rle_lt_dec 0 r) as [H1 | H1] ; [| exfalso ; destruct (Hf 0) ; try apply Cv_radius_weak_0] ; 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