proposition: Lemma n_deriv_I_wd'' : forall n a b Hab Hab' F H H' x y, x [=] y -> Compact (less_leEq _ _ _ Hab) x -> Compact (less_leEq _ _ _ Hab) y -> forall Hx Hy, n_deriv_I a b Hab n F H x Hx [=] n_deriv_I a b Hab' n F H' y Hy.
proof: Proof. intros n a b Hab Hab' F H H' x y H0 H1 H2 Hx Hy. apply n_deriv_I_wd'. algebra. auto. auto. apply included_imp_diffble_n with (Hab' := Hab). 2: auto. intros x0 H3. elim H3; clear H3; intros H4 H5; split. eapply leEq_wdl. apply H4. apply Min_id. eapply leEq_wdr. apply H5. apply Max_id. Qed.
imports: CoRN.ftc.Differentiability