proposition: Lemma N_Deriv_Feq : forall n F diffF a b Hab H (incN : included (Compact (less_leEq _ _ _ Hab)) (Dom (N_Deriv n F diffF))), Feq (Compact (less_leEq _ _ _ Hab)) (N_Deriv n F diffF) (n_deriv_I a b Hab n F H).
proof: Proof. intros. FEQ. apply n_deriv_inc. simpl in |- *. cut (Diffble_I_n (proper_compact_in_interval' _ _ _ _ (compact_compact_in_interval I pI x Hx)) n F). intro H1. eapply eq_transitive_unfolded. apply (N_Deriv_char n F diffF x Hx H1). apply n_deriv_I_wd'; auto. algebra. apply iprop_compact_in_interval_inc2; apply iprop_compact_in_interval. apply included_imp_Diffble_n; auto. apply included_interval'. apply (included_compact_in_interval I pI x Hx). apply (iprop_compact_in_interval_inc1 _ _ _ _ (compact_compact_in_interval I pI x Hx) (Lend_leEq_Rend _ (compact_compact_in_interval I pI x Hx))). apply compact_inc_lft. apply (included_compact_in_interval I pI x Hx). apply (iprop_compact_in_interval_inc1 _ _ _ _ (compact_compact_in_interval I pI x Hx) (Lend_leEq_Rend _ (compact_compact_in_interval I pI x Hx))). apply compact_inc_rht. apply incN; apply compact_inc_lft. apply incN; apply compact_inc_rht. elim diffF; intros incF diffbleF. apply diffbleF; auto. eapply included_trans. apply iprop_compact_in_interval_inc1. Included. Qed.
imports: CoRN.ftc.MoreIntervals