proposition: Lemma included_imp_diffble_n : forall n c d Hcd F, included (Compact (less_leEq _ c d Hcd)) (Compact (less_leEq _ a b Hab')) -> Diffble_I_n Hab' n F -> Diffble_I_n Hcd n F.
proof: Proof. intro; induction n as [| n Hrecn]; simpl in |- *; intros c d Hcd F H H0. apply included_trans with (Compact (less_leEq _ _ _ Hab')); Included. elim H0; intros f' HF. exists (included_imp_diffble _ _ _ _ _ _ _ H f'). apply Diffble_I_n_wd with (PartInt (ProjT1 f')). apply Derivative_I_unique with F. apply included_imp_deriv with (Hab := Hab'). auto. apply projT2. apply projT2. auto. Qed.
imports: CoRN.ftc.Differentiability