proposition: Lemma N_Deriv_strext : forall x y Hx Hy, N_Deriv_fun x Hx [#] N_Deriv_fun y Hy -> x [#] y.
proof: Proof. intros x y Hx Hy H. elim diffF; intros incF diffbleF. cut (Diffble_I_n (proper_compact_in_interval2' _ _ _ _ _ _ (compact_compact_in_interval2 I pI x y Hx Hy)) n F). intro H0. cut (Diffble_I_n (proper_compact_in_interval' _ _ _ _ (compact_compact_in_interval I pI x Hx)) n F). intro H1. cut (Diffble_I_n (proper_compact_in_interval' _ _ _ _ (compact_compact_in_interval I pI y Hy)) n F). intro H2. cut (Dom (n_deriv_I _ _ _ _ _ H0) x). intro H3. cut (Dom (n_deriv_I _ _ _ _ _ H0) y). intro H4. apply pfstrx with (Hx := H3) (Hy := H4). eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply H. eapply eq_transitive_unfolded. apply (N_Deriv_char y Hy H2). apply n_deriv_I_wd'. algebra. apply iprop_compact_in_interval_inc2; apply iprop_compact_in_interval. apply iprop_compact_in_interval2_inc2; apply iprop_compact_in_interval2y. apply included_imp_diffble_n with (Hab' := proper_compact_in_interval2' _ _ _ _ _ _ (compact_compact_in_interval2 I pI x y Hx Hy)). 2: apply H0. red in |- *; intros z Hz. inversion_clear Hz; split. eapply leEq_wdl. apply H5. eapply eq_transitive_unfolded. apply Min_comm. apply leEq_imp_Min_is_lft. apply compact_in_interval_y_lft. eapply leEq_wdr. apply H6. apply leEq_imp_Max_is_rht. apply compact_in_interval_y_rht. eapply eq_transitive_unfolded. apply (N_Deriv_char x Hx H1). apply n_deriv_I_wd'. algebra. apply iprop_compact_in_interval_inc2; apply iprop_compact_in_interval. apply iprop_compact_in_interval2_inc2; apply iprop_compact_in_interval2x. apply included_imp_diffble_n with (Hab' := proper_compact_in_interval2' _ _ _ _ _ _ (compact_compact_in_interval2 I pI x y Hx Hy)). 2: apply H0. red in |- *; intros z Hz. inversion_clear Hz; split. eapply leEq_wdl. apply H5. eapply eq_transitive_unfolded. apply Min_comm. apply leEq_imp_Min_is_lft. apply compact_in_interval_x_lft. eapply leEq_wdr. apply H6. apply leEq_imp_Max_is_rht. apply compact_in_interval_x_rht. apply n_deriv_inc. apply iprop_compact_in_interval2_inc2; apply iprop_compact_in_interval2y. apply n_deriv_inc. apply iprop_compact_in_interval2_inc2; apply iprop_compact_in_interval2x. apply diffbleF. simpl in |- *; Included. apply diffbleF. simpl in |- *; Included. apply diffbleF. simpl in |- *; Included. Qed.
imports: CoRN.ftc.MoreIntervals