proposition: Lemma nth_derive_sum_PI_O : forall an (r1 r2 : infinite_cv_radius an), nth_derive (sum an r1) (D_infty_Rpser an r1 O) == sum an r2.
proof: Proof. intros an r1 r2 ; apply sum_ext ; reflexivity. 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