proposition: Lemma Rdiv_exp_seq_simpl : forall n, (exp_seq (S n)) / (exp_seq n) = / INR (S n).
proof: Proof. intros n ; unfold exp_seq. replace (fact (S n))%nat with ((S n) * fact n)%nat by reflexivity ; unfold Rdiv ; rewrite mult_INR, Rinv_involutive ; [rewrite Rinv_mult_distr ; [rewrite Rmult_assoc, Rinv_l, Rmult_1_r ; [reflexivity |] | |] |] ; apply not_0_INR ; auto ; apply fact_neq_0. 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