proposition: Lemma Cv_radius_weak_shift_compat : forall An r, Cv_radius_weak An r <-> Cv_radius_weak (Rseq_shift An) r.
proof: Proof. intros An r ; replace (Rseq_shift An) with (Rseq_shifts An 1) by reflexivity ; apply Cv_radius_weak_shifts_compat. 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