proposition: Lemma identity_is_id : forall (ri : infinite_cv_radius identity_seq) (di : derivable (sum _ ri)), forall x, derive (sum _ ri) di x = 1.
proof: Proof. intros ri di ; solve_diff_equa ; unfold An_deriv, identity_seq, constant_seq, Rseq_shift, Rseq_mult ; intros [ | n] ; simpl ; ring. 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