proposition: Lemma infinite_cv_radius_expand_compat : forall An l, infinite_cv_radius An -> infinite_cv_radius (An_expand An l).
proof: Proof. intros ; intro r ; rewrite <- Cv_radius_weak_expand_compat ; trivial. 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