proposition: Lemma finite_cv_radius_nth_derivable_compat (k : nat) : forall An r, finite_cv_radius An r <-> finite_cv_radius (An_nth_deriv An k) r.
proof: Proof. induction k ; intros An r. rewrite <- finite_cv_radius_ext ; [reflexivity | apply An_nth_deriv_0]. split ; intro Rho. rewrite finite_cv_radius_ext ; [| eapply An_nth_deriv_S]. rewrite <- finite_cv_radius_derivable_compat, <- IHk ; assumption. rewrite IHk, finite_cv_radius_derivable_compat ; rewrite <- finite_cv_radius_ext ; [| eapply An_nth_deriv_S] ; assumption. 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