proposition: Lemma included_imp_diffble : forall a b Hab c d Hcd F, included (compact c d (less_leEq _ _ _ Hcd)) (compact a b (less_leEq _ _ _ Hab)) -> Diffble_I Hab F -> Diffble_I Hcd F.
proof: Proof. intros a b Hab c d Hcd F H H0. elim H0; clear H0; intros f' derF. exists (IntPartIR (F:=(Frestr (F:=PartInt f') (compact_wd _ _ _) H)) (included_refl _ _)). apply Derivative_I_wdr with (PartInt f'). FEQ. simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. exact (included_imp_deriv _ _ _ _ _ _ _ _ H derF). Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps