proposition: Theorem Law_of_the_Mean : forall a b, I a -> I b -> forall e, [0] [<] e -> {x : IR | Compact (Min_leEq_Max a b) x | forall Ha Hb Hx, AbsIR (F b Hb[-]F a Ha[-]F' x Hx[*] (b[-]a)) [<=] e}.
proof: Proof. intros a b Ha Hb e He. cut (included (Compact (Min_leEq_Max a b)) I). intro H. 2: apply included_interval'; auto. elim (less_cotransitive_unfolded _ _ _ He (AbsIR (F b (incF _ Hb) [-]F a (incF _ Ha) [-]F' a (incF' _ Ha) [*] (b[-]a)))); intros. cut (Min a b [<] Max a b). intro H0. cut (included (Compact (less_leEq _ _ _ H0)) I). intro H1. 2: apply included_interval'; auto. elim (ap_imp_less _ _ _ (Min_less_Max_imp_ap _ _ H0)); intro. cut (included (Compact (less_leEq _ _ _ a1)) I). intro H2. 2: apply included_trans with (Compact (less_leEq _ _ _ H0)); [ apply compact_map2 | apply H1 ]. elim (Law_of_the_Mean_I _ _ a1 _ _ (included_imp_Derivative _ _ _ _ derF _ _ a1 H2) ( incF _ Ha) (incF _ Hb) e He). intros x H3 H4. exists x; auto. apply compact_map2 with (Hab := less_leEq _ _ _ a1); auto. intros. eapply leEq_wdl. apply (H4 Hx). apply AbsIR_wd; algebra. cut (included (Compact (Min_leEq_Max b a)) (Compact (Min_leEq_Max a b))). intro H2. cut (included (Compact (less_leEq _ _ _ b0)) I). intro H3. 2: apply included_trans with (Compact (Min_leEq_Max b a)); [ apply compact_map2 | apply included_trans with (Compact (less_leEq _ _ _ H0)); [ apply H2 | apply H1 ] ]. elim (Law_of_the_Mean_I _ _ b0 _ _ (included_imp_Derivative _ _ _ _ derF _ _ b0 H3) ( incF _ Hb) (incF _ Ha) e He). intros x H4 H5. exists x; auto. apply H2; apply compact_map2 with (Hab := less_leEq _ _ _ b0); auto. intros. eapply leEq_wdl. apply (H5 Hx). eapply eq_transitive_unfolded. apply AbsIR_minus. apply AbsIR_wd; rational. intros x H2. elim H2; clear H2; intros H3 H4; split. eapply leEq_wdl; [ apply H3 | apply Min_comm ]. eapply leEq_wdr; [ apply H4 | apply Max_comm ]. apply ap_imp_Min_less_Max. cut (Part _ _ (incF b Hb) [-]Part _ _ (incF a Ha) [#] [0] or Part _ _ (incF' a Ha) [*] (b[-]a) [#] [0]). intro H0. elim H0; clear H0; intro H1. apply pfstrx with F (incF a Ha) (incF b Hb). apply ap_symmetric_unfolded; apply zero_minus_apart; auto. apply ap_symmetric_unfolded; apply zero_minus_apart. eapply cring_mult_ap_zero_op; apply H1. apply cg_minus_strext. astepr ZeroR. apply AbsIR_cancel_ap_zero. apply Greater_imp_ap; auto. exists a. apply compact_Min_lft. intros; apply less_leEq. eapply less_wdl. apply b0. apply AbsIR_wd; algebra. Qed.
imports: CoRN.tactics.DiffTactics2 CoRN.ftc.MoreFunctions