proposition: Lemma Included_imp_Derivative_n : forall n (J : interval) pJ F F', included J I -> Derivative_n n I pI F F' -> Derivative_n n J pJ F F'.
proof: Proof. intros n J pJ F F' H H0. elim H0; clear H0; intros H1 H2. elim H2; clear H2; intros H0 H3. split. Included. split. Included. intros; apply H3. Included. Qed.
imports: CoRN.ftc.MoreIntervals