proposition: Lemma Cv_radius_weak_alt : forall An r, Cv_radius_weak An r <-> Cv_radius_weak (Rseq_alt An) r.
proof: Proof. intros An r ; split ; intro rAn. eapply Cv_radius_weak_abs, Cv_radius_weak_ext. apply Rseq_abs_alt. rewrite <- Cv_radius_weak_abs ; assumption. rewrite Cv_radius_weak_abs, Cv_radius_weak_ext with (Bn := Rseq_abs (Rseq_alt An)). rewrite <- Cv_radius_weak_abs ; assumption. symmetry ; apply Rseq_abs_alt. 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