proposition: Lemma included_imp_deriv_n : forall n c d Hcd F F', included (Compact (less_leEq _ c d Hcd)) (Compact (less_leEq _ a b Hab')) -> Derivative_I_n Hab' n F F' -> Derivative_I_n Hcd n F F'.
proof: Proof. intro; induction n as [| n Hrecn]; simpl in |- *; intros c d Hcd F F' H H0. apply included_Feq with (Compact (less_leEq _ _ _ Hab')); auto. elim H0; intros f' H1 H2. 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. apply included_imp_deriv with (Hab := Hab'); auto. apply Derivative_I_n_wdl with (PartInt f'). FEQ. simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. auto. Qed.
imports: CoRN.ftc.Differentiability