proposition: Lemma Derivative_n_chain : forall F f, Feq I F (f 0) -> (forall n, Derivative I pI (f n) (f (S n))) -> forall n, Derivative_n n I pI F (f n).
proof: Proof. intros F f H H0 n. induction n as [| n Hrecn]. apply Derivative_n_wdr with F. auto. apply Derivative_n_O. elim H; auto. apply Derivative_n_plus with 1 n (f n); auto. apply Derivative_n_1; auto. rewrite Nat.add_comm; auto. Qed.
imports: CoRN.ftc.MoreIntervals