proposition: Lemma An_nth_deriv_1 : forall An, An_nth_deriv An 1 == An_deriv An.
proof: Proof. intros An n ; rewrite An_nth_deriv_S ; unfold An_deriv, Rseq_mult, Rseq_shift ; rewrite An_nth_deriv_0 ; reflexivity. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def