proposition: Lemma An_nth_deriv_0 : forall An, An_nth_deriv An 0 == An.
proof: Proof. intros An n ; unfold An_nth_deriv, Rseq_shifts, Rseq_div, Rseq_mult, Rdiv ; rewrite Nat.add_0_l ; field ; apply not_0_INR ; apply fact_neq_0. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def