proposition: Lemma Diffble_Int : forall (I : interval) (cI : compact_ I) (pI : proper I) H (F : PartIR), Diffble_I (a:=Lend cI) (b:=Rend cI) H F -> Diffble I pI 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 pI cI. 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 X1; clear X1 F X0 X H pI cI c0 c. simpl in |- *; intros a b Hab Hnonv Hab' inc1 inc2 F diffF. red in |- *; simpl in |- *. split. apply included_trans with (Compact (less_leEq _ _ _ Hab')); Included. intros c d Hcd' Hinc. apply included_imp_diffble with (Hab := Hab'); auto. Qed.
imports: CoRN.ftc.NthDerivative