proposition: Lemma nth_derive_sum_PI': forall (n : nat) an (r1 r2 : infinite_cv_radius an) (pr : D n (sum an r2)), (fun x => nth_derive (sum an r1) (D_infty_Rpser an r1 n) (1 * x)) == nth_derive (sum an r2) pr.
proof: Proof. intros n an r1 r2 pr x ; rewrite Rmult_1_l ; apply nth_derive_sum_PI. Qed.
imports: List Rsequence_def Rpser_def Rpser_def_simpl Rpser_sums Rpser_derivative Rpser_usual Rfunction_classes Nth_derivative_def Nth_derivative_facts Dequa_def Dequa_facts Rfunction_def Rextensionality