proposition: Lemma Deriv_exp_seq_simpl : (An_deriv exp_seq == exp_seq)%Rseq.
proof: Proof. intro n ; unfold exp_seq, An_deriv, Rseq_shift, Rseq_mult. replace (fact (S n))%nat with ((S n) * fact n)%nat by reflexivity. rewrite mult_INR, Rinv_mult_distr, <- Rmult_assoc, Rinv_r, Rmult_1_l ; [reflexivity | | |] ; replace 0 with (INR O) by reflexivity ; apply not_INR ; try apply fact_neq_0 ; intuition. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity