proposition: Lemma included_imp_Derivative_n : forall n F F' a b Hab, Derivative_n n I pI F F' -> included (Compact (less_leEq _ a b Hab)) I -> Derivative_I_n Hab n F F'.
proof: Proof. intros n F F' a b Hab H H0. elim H; intros incF H1. elim H1; auto. Qed.
imports: CoRN.ftc.MoreIntervals