proposition: Lemma infinite_cv_radius_shift_compat : forall An, infinite_cv_radius (Rseq_shift An) <-> infinite_cv_radius An.
proof: Proof. intro An ; split ; intros rAn r ; [ rewrite Cv_radius_weak_shift_compat | rewrite <- Cv_radius_weak_shift_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