proposition: Lemma n_deriv_I_strext' : forall n a b Hab a' b' Hab' F H H' 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) -> x [#] y.
proof: Proof. intros n a b Hab a' b' Hab' F H H' x y H0 H1 H2 H3. cut (Compact (less_leEq _ _ _ (Min_less_Max a b a' b' Hab)) x). intro H4. cut (Compact (less_leEq _ _ _ (Min_less_Max a b a' b' Hab)) y). intro H5. apply pfstrx with (n_deriv_I _ _ _ _ _ H2) (n_deriv_inc _ _ _ _ _ H2 _ H4) (n_deriv_inc _ _ _ _ _ H2 _ H5). apply ap_wdr_unfolded with (Part (n_deriv_I _ _ _ _ _ H') y (n_deriv_inc _ _ _ _ _ H' y H1)). apply ap_wdl_unfolded with (Part (n_deriv_I _ _ _ _ _ H) x (n_deriv_inc _ _ _ _ _ H x H0)). auto. apply Feq_imp_eq with (Compact (less_leEq _ _ _ Hab)). apply Derivative_I_n_unique with n F. apply n_deriv_lemma. 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. apply Feq_imp_eq with (Compact (less_leEq _ _ _ Hab')). apply Derivative_I_n_unique with n F. apply n_deriv_lemma. 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. elim H1; clear H1; intros H7 H8; split. apply leEq_transitive with a'. apply Min_leEq_rht. auto. apply leEq_transitive with b'. auto. apply rht_leEq_Max. red in |- *; intros. inversion_clear H0; 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