proposition: Lemma An_nth_deriv_S : forall An k, An_nth_deriv An (S k) == An_deriv (An_nth_deriv An k).
proof: Proof. assert (Hrew : forall n, / Rseq_fact n = INR (S n) * / Rseq_fact (S n)). intro n ; unfold Rseq_fact ; rewrite fact_simpl, mult_INR, Rinv_mult, <- Rmult_assoc. symmetry ; apply Rinv_r_simpl_r ; apply not_0_INR ; lia. intros An k n ; unfold An_nth_deriv, An_deriv, Rseq_shift, Rseq_shifts, Rseq_div, Rseq_mult, Rdiv ; rewrite Hrew, <- plus_n_Sm. simpl ; ring. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def