proposition: Lemma Cv_radius_weak_nth_derivable_compat_rev (k : nat) : forall An r, Cv_radius_weak (An_nth_deriv An k) r -> Cv_radius_weak An r.
proof: Proof. induction k ; intros An r rAn. erewrite Cv_radius_weak_ext. eassumption. symmetry ; apply An_nth_deriv_0. apply IHk ; apply Cv_radius_weak_derivable_compat_rev ; erewrite Cv_radius_weak_ext. eassumption. symmetry ; apply An_nth_deriv_S. Qed.
imports: Reals Fourier Lra Rpow_facts Rinterval Rextensionality Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts RFsequence RFsequence_facts Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_sums MyINR