proposition: Lemma finite_cv_radius_alt_compat : forall (An : Rseq) (r : R), finite_cv_radius An r <-> finite_cv_radius (Rseq_alt An) r.
proof: Proof. intros An r ; split ; intros [r_ub r_lub] ; split. intros ; rewrite <- Cv_radius_weak_alt ; apply r_ub ; assumption. intros ; rewrite <- Cv_radius_weak_alt ; apply r_lub ; assumption. intros ; apply Cv_radius_weak_alt, r_ub ; assumption. intros ; rewrite Cv_radius_weak_alt ; apply r_lub ; 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