proposition: Lemma Int_Derivative : forall (I : interval) (cI : compact_ I) (pI : proper I) H (F F' : PartIR), Derivative I pI F F' -> Derivative_I (a:=Lend cI) (b:=Rend cI) H F F'.
proof: Proof. intros [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI. generalize c c0 cI pI H F F' X; clear X F' F H pI cI c0 c. simpl in |- *; intros a b Hab Hnonv Hab' F F' derF. elim derF; intros H H0. elim H0; intros H1 H2. Included. Qed.
imports: CoRN.ftc.NthDerivative