proposition: Lemma CV_radius_derive_n (n : nat) (a : nat -> R) : CV_radius (PS_derive_n n a) = CV_radius a.
proof: Proof. elim: n a => [ | n IH] /= a. apply CV_radius_ext. move => k ; rewrite /PS_derive_n /=. rewrite Nat.add_0_r ; field. by apply INR_fact_neq_0. rewrite -(CV_radius_derive a). rewrite -(IH (PS_derive a)). apply CV_radius_ext. move => k ; rewrite /PS_derive_n /PS_derive. rewrite -plus_n_Sm /fact -/fact mult_INR ; field. by apply INR_fact_neq_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series