proposition: Lemma Derivative_Int : forall (I : interval) (cI : compact_ I) (pI : proper I) H (F F' : PartIR), Derivative_I (a:=Lend cI) (b:=Rend cI) H F F' -> Derivative I pI F F'.
proof: Proof. do 4 intro. cut (included I (compact (Lend cI) (Rend cI) (less_leEq _ _ _ H))). 2: apply interval_compact_inc; auto. cut (included (compact (Lend cI) (Rend cI) (less_leEq _ _ _ H)) I). 2: apply compact_interval_inc; auto. generalize cI pI H; clear H cI pI. destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI. generalize c c0 cI pI H X X0 F F' X1; clear X1 F' F X0 X H pI cI c0 c. simpl in |- *; intros a b Hab Hnonv Hab' inc1 inc2 F F' derF. split. apply included_trans with (Compact (less_leEq _ _ _ Hab')); Included. split. apply included_trans with (Compact (less_leEq _ _ _ Hab')); Included. intros c d Hcd' Hinc. apply included_imp_deriv with (Hab := Hab'); Included. Qed.
imports: CoRN.ftc.NthDerivative