proposition: Lemma Law_of_the_Mean_I : forall e, [0] [<] e -> {x : IR | I x | forall Hx, AbsIR (F b HB[-]F a HA[-]F' x Hx[*] (b[-]a)) [<=] e}.
proof: Proof. intros e H. set (h := (FId{-} [-C-]a) {*} [-C-] (F b HB[-]F a HA) {-}F{*} [-C-] (b[-]a)) in *. set (h' := [-C-] (F b HB[-]F a HA) {-}F'{*} [-C-] (b[-]a)) in *. cut (Derivative_I Hab' h h'). intro H0. cut {x : IR | I x | forall Hx, AbsIR (h' x Hx) [<=] e}. intro H1. elim H1; intros x Ix Hx. exists x. assumption. intro. eapply leEq_wdl. apply (Hx (derivative_imp_inc' _ _ _ _ _ H0 x Ix)). apply AbsIR_wd; simpl in |- *; rational. unfold I, Hab in |- *; eapply Rolle with h (derivative_imp_inc _ _ _ _ _ H0 _ (compact_inc_lft _ _ _)) (derivative_imp_inc _ _ _ _ _ H0 _ (compact_inc_rht _ _ _)). assumption. simpl in |- *; rational. assumption. unfold h, h' in |- *; clear h h'. New_Deriv. apply Feq_reflexive. apply included_FMinus; Included. apply eq_imp_Feq. apply included_FMinus. apply included_FPlus; Included. Included. Included. intros. simpl in |- *; rational. Qed.
imports: CoRN.tactics.DiffTactics2 CoRN.ftc.MoreFunctions