proposition: Lemma Included_imp_Derivative : forall J (pJ : proper J), included J I -> Derivative J pJ F F'.
proof: Proof. intros J pJ H. split. exact (included_trans _ _ _ _ H (Derivative_imp_inc _ _ _ _ derF)). split. exact (included_trans _ _ _ _ H (Derivative_imp_inc' _ _ _ _ derF)). intros. apply included_imp_Derivative; Included. Qed.
imports: CoRN.ftc.MoreIntervals