proposition: Lemma infinite_cv_radius_nth_derivable_compat (k : nat) : forall An, infinite_cv_radius An <-> infinite_cv_radius (An_nth_deriv An k).
proof: Proof. induction k ; intro An. rewrite <- infinite_cv_radius_ext ; [| eapply An_nth_deriv_0] ; reflexivity. split ; intro Rho. rewrite infinite_cv_radius_ext ; [| eapply An_nth_deriv_S]. rewrite <- infinite_cv_radius_derivable_compat, <- IHk ; assumption. rewrite IHk, infinite_cv_radius_derivable_compat, <- infinite_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