proposition: Lemma Int_Diffble : forall (I : interval) (cI : compact_ I) (pI : proper I) H (F : PartIR), Diffble I pI F -> Diffble_I (a:=Lend cI) (b:=Rend cI) H 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 X; clear X F H pI cI c0 c. simpl in |- *; intros a b Hab Hnonv Hab' F diffF. inversion_clear diffF. Included. Qed.
imports: CoRN.ftc.NthDerivative