proposition: Lemma Cdiv_exp_seq_simpl : forall n, (exp_seq (S n)) / (exp_seq n) = / INC (S n).
proof: Proof. intros n ; unfold exp_seq. replace (fact (S n))%nat with ((S n) * fact n)%nat by reflexivity ; unfold Cdiv ; rewrite mult_INC, Cinv_involutive ; [rewrite Cinv_mult_distr ; [rewrite Cmult_assoc, Cinv_l, Cmult_1_r ; [reflexivity |] | |] |] ; apply not_0_INC ; auto ; apply fact_neq_0. 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