proposition: Lemma diff_equa_exp : forall n (re : infinite_cv_radius exp_seq) x, nth_derive (sum _ re) (D_infty_Rpser _ re (S n)) x = nth_derive (sum _ re) (D_infty_Rpser _ re n) x.
proof: Proof. intros n re ; solve_diff_equa ; rewrite An_nth_deriv_S', (An_nth_deriv_ext _ exp_seq) ; [reflexivity | apply Deriv_exp_seq_simpl]. Qed.
imports: Rsequence_def Rsequence_base_facts Reals Rfunction_def Rfunction_facts Rextensionality Nth_derivative_def Nth_derivative_facts Rpser Rfunction_classes Dequa_def Dequa_facts Dequa_quote List