proposition: Lemma n_deriv_I_wd' : forall n a b Hab a' b' Hab' F H H' x y, x [=] y -> Compact (less_leEq _ _ _ Hab) x -> Compact (less_leEq _ _ _ Hab') y -> Diffble_I_n (Min_less_Max _ _ a' b' Hab) n F -> 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 a' b' Hab' F H H' x y H0 H1 H2 H3 Hx Hy. cut (included (Compact (less_leEq _ _ _ Hab)) (Dom (n_deriv_I _ _ _ _ _ H3))). intro H4. cut (included (Compact (less_leEq _ _ _ Hab')) (Dom (n_deriv_I _ _ _ _ _ H3))). intro H5. apply eq_transitive_unfolded with (Part (FRestr H5) y H2). apply eq_transitive_unfolded with (Part (FRestr H4) x H1). apply Feq_imp_eq with (Compact (less_leEq _ _ _ Hab)). apply Derivative_I_n_unique with n F. apply n_deriv_lemma. apply Derivative_I_n_wdr with (n_deriv_I _ _ _ _ _ H3). FEQ. apply included_imp_deriv_n with (Hab' := Min_less_Max a b a' b' Hab). intros x0 H6. elim H6; clear H6; intros H7 H8; split. apply leEq_transitive with a. apply Min_leEq_lft. auto. apply leEq_transitive with b. auto. apply lft_leEq_Max. apply n_deriv_lemma. auto. simpl in |- *; algebra. apply eq_symmetric_unfolded. apply Feq_imp_eq with (Compact (less_leEq _ _ _ Hab')). apply Derivative_I_n_unique with n F. apply n_deriv_lemma. apply Derivative_I_n_wdr with (n_deriv_I _ _ _ _ _ H3). FEQ. apply included_imp_deriv_n with (Hab' := Min_less_Max a b a' b' Hab). intros x0 H6. elim H6; clear H6; intros H7 H8; split. apply leEq_transitive with a'. apply Min_leEq_rht. auto. apply leEq_transitive with b'. auto. apply rht_leEq_Max. apply n_deriv_lemma. auto. intros x0 H5. apply n_deriv_inc. elim H5; clear H5; intros H6 H7; split. apply leEq_transitive with a'. apply Min_leEq_rht. auto. apply leEq_transitive with b'. auto. apply rht_leEq_Max. intros x0 H4. apply n_deriv_inc. elim H4; clear H4; intros H5 H6; split. apply leEq_transitive with a. apply Min_leEq_lft. auto. apply leEq_transitive with b. auto. apply lft_leEq_Max. Qed.
imports: CoRN.ftc.Differentiability