proposition: Lemma An_nth_deriv_S' : forall An k, An_nth_deriv An (S k) == An_nth_deriv (An_deriv An) k.
proof: Proof. intros An k n ; unfold An_nth_deriv, An_deriv, Rseq_shift, Rseq_shifts, Rseq_mult, Rseq_div, Rdiv ; simpl (S k + n)%nat ; rewrite Rseq_fact_simpl ; ring. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def