proposition: Lemma Derivative_nth : forall n, Derivative I pI (F{^}S n) (nring (S n) {**} (F'{*}F{^}n)).
proof: Proof. elim derF; intros incF H. elim H; intros incF' derivF. split. Included. split; Deriv. Qed.
imports: CoRN.ftc.MoreIntervals