proposition: Lemma Deriv_exp_seq_simpl : forall n, An_deriv exp_seq n = exp_seq n.
proof: Proof. intro n ; unfold exp_seq, An_deriv, Cseq_shift, Cseq_mult. replace (fact (S n))%nat with ((S n) * fact n)%nat by reflexivity. rewrite mult_INC, Cinv_mult_distr, <- Cmult_assoc, Cinv_r, Cmult_1_l ; [reflexivity | | |] ; replace C0 with (INC O) by reflexivity ; apply not_INC ; try apply fact_neq_0 ; intuition. Qed.
imports: Lia Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_usual_facts Rtactic MyRIneq Cprop_base Csequence Csequence_facts Cpser_def Cpser_base_facts Cpser_facts Cseries Cseries_facts Cdefinitions Canalysis_def