proposition: Lemma N_Deriv_char : forall x Hx H, N_Deriv_fun x Hx [=] Part (n_deriv_I _ _ (proper_compact_in_interval' _ _ _ _ (compact_compact_in_interval I pI x Hx)) n F H) x (n_deriv_inc _ _ _ _ _ _ _ (iprop_compact_in_interval_inc2 _ _ _ _ (compact_compact_in_interval _ _ _ _) (less_leEq _ _ _ (proper_compact_in_interval' _ _ _ _ (compact_compact_in_interval _ _ _ _))) _ (iprop_compact_in_interval _ _ _ _))).
proof: Proof. intros. unfold N_Deriv_fun in |- *. elim diffF; intros; simpl in |- *. apply n_deriv_I_wd'. algebra. apply iprop_compact_in_interval'. apply iprop_compact_in_interval'. apply b. apply included_trans with (Compact (less_leEq _ _ _ (proper_compact_in_interval' _ _ _ _ (compact_compact_in_interval I pI x Hx)))). 2: Included. intros x0 H0. inversion_clear H0. split. eapply leEq_wdl. apply H1. eapply eq_transitive_unfolded. apply Min_comm. apply leEq_imp_Min_is_lft; apply eq_imp_leEq. apply compact_in_interval_wd1; algebra. eapply leEq_wdr. apply H2. apply leEq_imp_Max_is_rht; apply eq_imp_leEq. apply compact_in_interval_wd2; algebra. Qed.
imports: CoRN.ftc.MoreIntervals