Rolle.v

(* Copyright © 1998-2006
 * Henk Barendregt
 * Luís Cruz-Filipe
 * Herman Geuvers
 * Mariusz Giero
 * Rik van Ginneken
 * Dimitri Hendriks
 * Sébastien Hinderer
 * Bart Kirkels
 * Pierre Letouzey
 * Iris Loeb
 * Lionel Mamane
 * Milad Niqui
 * Russell O’Connor
 * Randy Pollack
 * Nickolay V. Shmyrev
 * Bas Spitters
 * Dan Synek
 * Freek Wiedijk
 * Jan Zwanenburg
 *
 * This work is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This work is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License along
 * with this work; if not, write to the Free Software Foundation, Inc.,
 * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 *)

Require Export CoRN.tactics.DiffTactics2.
Require Export CoRN.ftc.MoreFunctions.

Section Rolle.

(**
* Rolle's Theorem

We now begin to work with partial functions.  We begin by stating and proving Rolle's theorem in various forms and some of its corollaries.

%\begin{convention}% Assume that:
 - [a,b:IR] with [a [<] b] and denote by [I] the interval [[a,b]];
 - [F,F'] are partial functions such that [F'] is the derivative of [F] in [I];
 - [e] is a positive real number.

%\end{convention}%
*)

(* begin hide *)
Variables a b : IR.
Hypothesis Hab' : a [<] b.

Let Hab := less_leEq _ _ _ Hab'.
Let I := Compact Hab.

Variables F F' : PartIR.

Hypothesis derF : Derivative_I Hab' F F'.
Hypothesis Ha : Dom F a.
Hypothesis Hb : Dom F b.
(* end hide *)

(* begin show *)
Hypothesis Fab : F a Ha [=] F b Hb.
(* end show *)

(* begin hide *)
Variable e : IR.
Hypothesis He : [0] [<] e.

Let contF' : Continuous_I Hab F'.
Proof.
 apply deriv_imp_contin'_I with Hab' F.
 assumption.
Qed.

Let derivF :
  forall e : IR,
  [0] [<] e ->
  {d : IR | [0] [<] d |
  forall x y : IR,
  I x ->
  I y ->
  forall Hx Hy Hx',
  AbsIR (x[-]y) [<=] d ->
  AbsIR (F y Hy[-]F x Hx[-]F' x Hx'[*] (y[-]x)) [<=] e[*]AbsIR (y[-]x)}.
Proof.
 elim derF.
 intros a0 b0.
 elim b0; intros H b1.
 unfold I in |- *; assumption.
Qed.

Let Rolle_lemma2 :
  {d : IR | [0] [<] d |
  forall x y : IR,
  I x ->
  I y ->
  forall Hx Hy Hx',
  AbsIR (x[-]y) [<=] d ->
  AbsIR (F y Hy[-]F x Hx[-]F' x Hx'[*] (y[-]x)) [<=] e [/]TwoNZ[*]AbsIR (y[-]x)}.
Proof.
 exact (derivF _ (pos_div_two _ _ He)).
Qed.

Let df := proj1_sig2T _ _ _ Rolle_lemma2.

Let Hdf : [0] [<] df := proj2a_sig2T _ _ _ Rolle_lemma2.

Let Hf :
  forall x y : IR,
  I x ->
  I y ->
  forall Hx Hy Hx',
  AbsIR (x[-]y) [<=] df ->
  AbsIR (F y Hy[-]F x Hx[-]F' x Hx'[*] (y[-]x)) [<=] e [/]TwoNZ[*]AbsIR (y[-]x) :=
  proj2b_sig2T _ _ _ Rolle_lemma2.

Let Rolle_lemma3 :
  {d : IR | [0] [<] d |
  forall x y : IR,
  I x ->
  I y ->
  forall Hx Hy, AbsIR (x[-]y) [<=] d -> AbsIR (F' x Hx[-]F' y Hy) [<=] e [/]TwoNZ}.
Proof.
 elim contF'; intros.
 exact (b0 _ (pos_div_two _ _ He)).
Qed.

Let df' := proj1_sig2T _ _ _ Rolle_lemma3.

Let Hdf' : [0] [<] df' := proj2a_sig2T _ _ _ Rolle_lemma3.

Let Hf' :
  forall x y : IR,
  I x ->
  I y ->
  forall Hx Hy,
  AbsIR (x[-]y) [<=] df' -> AbsIR (F' x Hx[-]F' y Hy) [<=] e [/]TwoNZ :=
  proj2b_sig2T _ _ _ Rolle_lemma3.

Let d := Min df df'.

Let Hd : [0] [<] d.
Proof.
 unfold d in |- *; apply less_Min; auto.
Qed.

Let incF : included (Compact Hab) (Dom F).
Proof.
 elim derF; intros; assumption.
Qed.

Let n := compact_nat a b d Hd.

Let fcp (i : nat) (Hi : i <= n) :=
  F (compact_part a b Hab' d Hd i Hi)
    (incF _ (compact_part_hyp a b Hab Hab' d Hd i Hi)).

Let Rolle_lemma1 :
  Sumx (fun (i : nat) (H : i < n) => fcp (S i) H[-]fcp i (Nat.lt_le_incl i n H)) [=]
  [0].
Proof.
 apply eq_transitive_unfolded with (fcp _ (le_n n) [-]fcp 0 (Nat.le_0_l n)).
  apply Mengolli_Sum with (f := fun (i : nat) (H : i <= n) => fcp _ H).
   red in |- *; do 3 intro.
   rewrite H; intros.
   unfold fcp in |- *; simpl in |- *; algebra.
  intros; algebra.
 apply eq_transitive_unfolded with (F b Hb[-]F a Ha).
  unfold fcp, compact_part, n in |- *; simpl in |- *.
  apply cg_minus_wd; apply pfwdef; rational.
 astepr (F a Ha[-]F a Ha); apply cg_minus_wd.
  apply eq_symmetric_unfolded; apply Fab.
 algebra.
Qed.

Let incF' : included (Compact Hab) (Dom F').
Proof.
 elim derF; intros.
 elim b0; intros.
 assumption.
Qed.

Let fcp' (i : nat) (Hi : i <= n) :=
  F' (compact_part a b Hab' d Hd i Hi)
    (incF' _ (compact_part_hyp a b Hab Hab' d Hd i Hi)).

Notation cp := (compact_part a b Hab' d Hd).

Let Rolle_lemma4 :
  {i : nat |
  {H : i < n |
  [0] [<]
  (fcp' _ (Nat.lt_le_incl _ _ H) [+]e) [*] (cp (S i) H[-]cp i (Nat.lt_le_incl _ _ H))}}.
Proof.
 apply positive_Sumx with (f := fun (i : nat) (H : i < n) => (fcp' _ (Nat.lt_le_incl _ _ H) [+]e) [*]
   (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H))).
  red in |- *; do 3 intro.
  rewrite H; intros.
  unfold fcp' in |- *; algebra.
 apply less_wdl with (Sumx (fun (i : nat) (H : i < n) => fcp _ H[-]fcp _ (Nat.lt_le_incl _ _ H))).
  2: apply Rolle_lemma1.
 apply Sumx_resp_less.
  apply less_nring with (IR:COrdField); simpl in |- *; unfold n in |- *; apply pos_compact_nat; auto.
 intros.
 apply leEq_less_trans with ((fcp' i (Nat.lt_le_incl _ _ H) [+]e [/]TwoNZ) [*]
   (cp (S i) H[-]cp i (Nat.lt_le_incl _ _ H))).
  2: apply mult_resp_less.
   3: apply compact_less.
  2: apply plus_resp_less_lft.
  2: apply pos_div_two'; assumption.
 rstepl (fcp' i (Nat.lt_le_incl _ _ H) [*] (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H)) [+]
   (fcp _ H[-]fcp _ (Nat.lt_le_incl _ _ H) [-]
     fcp' i (Nat.lt_le_incl _ _ H) [*] (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H)))).
 eapply leEq_wdr.
  2: apply eq_symmetric_unfolded; apply ring_distl_unfolded.
 apply plus_resp_leEq_lft.
 apply leEq_wdr with (e [/]TwoNZ[*]AbsIR (cp (S i) H[-]cp i (Nat.lt_le_incl _ _ H))).
  2: apply mult_wd.
   2: algebra.
  2: apply AbsIR_eq_x.
  2: apply less_leEq; apply compact_less.
 eapply leEq_transitive.
  apply leEq_AbsIR.
 unfold fcp, fcp' in |- *; apply Hf.
   unfold I in |- *; apply compact_part_hyp.
  unfold I in |- *; apply compact_part_hyp.
 eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_minus.
 apply leEq_transitive with d.
  2: unfold d in |- *; apply Min_leEq_lft.
 eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_eq_x.
  apply compact_leEq.
 apply less_leEq; apply compact_less.
Qed.

Let Rolle_lemma5 : {i : nat | {H : i <= n | [--]e [<] fcp' _ H}}.
Proof.
 elim Rolle_lemma4; intros i Hi; elim Hi; clear Hi; intros Hi Hi'.
 exists i; exists (Nat.lt_le_incl _ _ Hi).
 astepl ([0][-]e); apply shift_minus_less.
 eapply mult_cancel_less.
  2: eapply less_wdl.
   2: apply Hi'.
  2: algebra.
 apply compact_less.
Qed.

Let Rolle_lemma6 :
  {i : nat |
  {H : i < n |
  (fcp' _ (Nat.lt_le_incl _ _ H) [-]e) [*] (cp (S i) H[-]cp i (Nat.lt_le_incl _ _ H)) [<]
  [0]}}.
Proof.
 apply negative_Sumx with (f := fun (i : nat) (H : i < n) => (fcp' _ (Nat.lt_le_incl _ _ H) [-]e) [*]
   (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H))).
  red in |- *; do 3 intro.
  rewrite H; intros.
  unfold fcp' in |- *; algebra.
 apply less_wdr with (Sumx (fun (i : nat) (H : i < n) => fcp _ H[-]fcp _ (Nat.lt_le_incl _ _ H))).
  2: apply Rolle_lemma1.
 apply Sumx_resp_less.
  apply less_nring with (IR:COrdField); simpl in |- *; unfold n in |- *; apply pos_compact_nat; auto.
 intros.
 apply less_leEq_trans with ((fcp' _ (Nat.lt_le_incl _ _ H) [-]e [/]TwoNZ) [*]
   (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H))).
  apply mult_resp_less.
   2: apply compact_less.
  unfold cg_minus in |- *; apply plus_resp_less_lft.
  apply inv_resp_less; apply pos_div_two'; assumption.
 rstepr (fcp' _ (Nat.lt_le_incl _ _ H) [*] (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H)) [+] [--] [--]
   (fcp _ H[-]fcp _ (Nat.lt_le_incl _ _ H) [-]
     fcp' _ (Nat.lt_le_incl _ _ H) [*] (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H)))).
 rstepl (fcp' _ (Nat.lt_le_incl _ _ H) [*] (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H)) [-]
   e [/]TwoNZ[*] (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H))).
 unfold cg_minus at 1 in |- *; apply plus_resp_leEq_lft.
 apply inv_resp_leEq; apply leEq_wdr with (e [/]TwoNZ[*]AbsIR (cp _ H[-]cp _ (Nat.lt_le_incl _ _ H))).
  2: apply mult_wd.
   2: algebra.
  2: apply AbsIR_eq_x.
  2: apply less_leEq; apply compact_less.
 eapply leEq_transitive.
  apply inv_leEq_AbsIR.
 unfold fcp, fcp' in |- *; apply Hf.
   unfold I in |- *; apply compact_part_hyp.
  unfold I in |- *; apply compact_part_hyp.
 eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_minus.
 apply leEq_transitive with d.
  2: unfold d in |- *; apply Min_leEq_lft.
 eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_eq_x.
  apply compact_leEq.
 apply less_leEq; apply compact_less.
Qed.

Let Rolle_lemma7 : {i : nat | {H : i <= n | fcp' _ H [<] e}}.
Proof.
 elim Rolle_lemma6; intros i Hi; elim Hi; clear Hi; intros Hi Hi'.
 exists i; exists (Nat.lt_le_incl _ _ Hi).
 astepr (e[+][0]); apply shift_less_plus'.
 eapply mult_cancel_less.
  2: eapply less_wdr.
   2: apply Hi'.
  2: algebra.
 apply shift_less_minus.
 astepl (cp _ (Nat.lt_le_incl _ _ Hi)).
 unfold compact_part in |- *.
 apply plus_resp_less_lft.
 apply mult_resp_less.
  simpl in |- *; apply less_plusOne.
 apply div_resp_pos.
  2: apply shift_less_minus; astepl a; auto.
 apply pos_compact_nat; auto.
Qed.

Let j := ProjT1 Rolle_lemma5.

Let Hj := ProjT1 (ProjT2 Rolle_lemma5).

Let Hj' : [--]e [<] fcp' _ Hj.
Proof.
 exact (ProjT2 (ProjT2 Rolle_lemma5)).
Qed.

Let k := ProjT1 Rolle_lemma7.

Let Hk := ProjT1 (ProjT2 Rolle_lemma7).

Let Hk' : fcp' _ Hk [<] e.
Proof.
 exact (ProjT2 (ProjT2 Rolle_lemma7)).
Qed.

Let Rolle_lemma8 :
  forall (i : nat) (H : i <= n),
  AbsIR (fcp' _ H) [<] e or e [/]TwoNZ [<] AbsIR (fcp' _ H).
Proof.
 intros.
 cut (e [/]TwoNZ [<] AbsIR (fcp' _ H) or AbsIR (fcp' _ H) [<] e).
  intro H0; inversion_clear H0; [ right | left ]; assumption.
 apply less_cotransitive_unfolded.
 apply pos_div_two'; assumption.
Qed.

Let Rolle_lemma9 :
  {m : nat | {Hm : m <= n | AbsIR (fcp' _ Hm) [<] e}}
  or (forall (i : nat) (H : i <= n), e [/]TwoNZ [<] AbsIR (fcp' _ H)).
Proof.
 set (P := fun (i : nat) (H : i <= n) => AbsIR (fcp' _ H) [<] e) in *.
 set (Q := fun (i : nat) (H : i <= n) => e [/]TwoNZ [<] AbsIR (fcp' _ H)) in *.
 apply finite_or_elim with (P := P) (Q := Q).
   red in |- *.
   intros i i' Hii'; rewrite Hii'; intros Hi Hi' HP.
   red in |- *; red in HP.
   eapply less_wdl.
    apply HP.
   apply AbsIR_wd; unfold fcp' in |- *; algebra.
  red in |- *.
  intros i i' Hii'; rewrite Hii'; intros Hi Hi' HQ.
  red in |- *; red in HQ.
  eapply less_wdr.
   apply HQ.
  apply AbsIR_wd; unfold fcp' in |- *; algebra.
 apply Rolle_lemma8.
Qed.

Let Rolle_lemma10 :
  {m : nat | {Hm : m <= n | AbsIR (fcp' _ Hm) [<] e}} ->
  {x : IR | I x | forall Hx, AbsIR (F' x Hx) [<=] e}.
Proof.
 intro H.
 elim H; intros m Hm; elim Hm; clear H Hm; intros Hm Hm'.
 exists (cp _ Hm).
  red in |- *; apply compact_part_hyp.
 intro; apply less_leEq; eapply less_wdl.
  apply Hm'.
 apply AbsIR_wd; unfold fcp' in |- *; algebra.
Qed.

Let Rolle_lemma11 :
  (forall (i : nat) (H : i <= n), e [/]TwoNZ [<] AbsIR (fcp' _ H)) ->
  (forall H : 0 <= n, fcp' _ H [<] [--] (e [/]TwoNZ)) ->
  forall (i : nat) (H : i <= n), fcp' _ H [<] [0].
Proof.
 intros H H0.
 cut (forall H : 0 <= n, fcp' _ H [<] [0]).
  intro.
  simple induction i.
   assumption.
  intros i' Hrec HSi'.
  astepr (e [/]TwoNZ[-]e [/]TwoNZ).
  apply shift_less_minus.
  cut (i' <= n).
   2: auto with arith.
  intro Hi'.
  apply less_leEq_trans with (fcp' _ HSi'[-]fcp' _ Hi').
   unfold cg_minus in |- *; apply plus_resp_less_lft.
   cut (e [/]TwoNZ [<] fcp' _ Hi' or fcp' _ Hi' [<] [--] (e [/]TwoNZ)).
    intro H2.
    elim H2; clear H2; intro H3.
     exfalso.
     cut (e [/]TwoNZ [<] [0]).
      apply less_antisymmetric_unfolded.
      apply pos_div_two; assumption.
     eapply less_transitive_unfolded; [ apply H3 | apply Hrec ].
    astepl ( [--][--] (e [/]TwoNZ)); apply inv_resp_less; assumption.
   cut (e [/]TwoNZ [<] AbsIR (fcp' _ Hi')).
    2: exact (H i' Hi').
   intro H2.
   apply less_AbsIR.
    apply pos_div_two; assumption.
   assumption.
  eapply leEq_transitive.
   apply leEq_AbsIR.
  unfold fcp' in |- *; apply Hf'.
    red in |- *; apply compact_part_hyp.
   red in |- *; apply compact_part_hyp.
  apply leEq_transitive with d.
   2: unfold d in |- *; apply Min_leEq_rht.
  eapply leEq_wdl.
   2: apply eq_symmetric_unfolded; apply AbsIR_eq_x.
   apply compact_leEq.
  apply less_leEq; apply compact_less.
 intro.
 eapply less_transitive_unfolded.
  apply (H0 H1).
 astepr ( [--]ZeroR); apply inv_resp_less; apply pos_div_two; assumption.
Qed.

Let Rolle_lemma12 :
  (forall (i : nat) (H : i <= n), e [/]TwoNZ [<] AbsIR (fcp' _ H)) ->
  (forall H : 0 <= n, e [/]TwoNZ [<] fcp' _ H) ->
  forall (i : nat) (H : i <= n), [0] [<] fcp' _ H.
Proof.
 intros H H0.
 cut (forall H : 0 <= n, [0] [<] fcp' _ H).
  intro.
  simple induction i.
   assumption.
  intros i' Hrec HSi'.
  astepl ( [--]ZeroR); astepr ( [--][--] (fcp' _ HSi')); apply inv_resp_less.
  astepr (e [/]TwoNZ[-]e [/]TwoNZ).
  apply shift_less_minus'.
  astepl (e [/]TwoNZ[-]fcp' _ HSi').
  cut (i' <= n).
   2: auto with arith.
  intro Hi'.
  apply less_leEq_trans with (fcp' _ Hi'[-]fcp' _ HSi').
   unfold cg_minus in |- *; apply plus_resp_less_rht.
   cut (e [/]TwoNZ [<] fcp' _ Hi' or fcp' _ Hi' [<] [--] (e [/]TwoNZ)).
    intro H2; elim H2; clear H2; intro H3.
     assumption.
    exfalso.
    cut ([0] [<] [--] (e [/]TwoNZ)).
     apply less_antisymmetric_unfolded.
     astepr ( [--]ZeroR); apply inv_resp_less; apply pos_div_two; assumption.
    eapply less_transitive_unfolded; [ apply (Hrec Hi') | apply H3 ].
   cut (e [/]TwoNZ [<] AbsIR (fcp' _ Hi')).
    2: exact (H i' Hi').
   intro.
   apply less_AbsIR.
    apply pos_div_two; assumption.
   assumption.
  eapply leEq_transitive.
   apply leEq_AbsIR.
  unfold fcp' in |- *; apply Hf'.
    red in |- *; apply compact_part_hyp.
   red in |- *; apply compact_part_hyp.
  apply leEq_transitive with d.
   2: unfold d in |- *; apply Min_leEq_rht.
  eapply leEq_wdl.
   2: apply eq_symmetric_unfolded; apply AbsIR_minus.
  eapply leEq_wdl.
   2: apply eq_symmetric_unfolded; apply AbsIR_eq_x.
   apply compact_leEq.
  apply less_leEq; apply compact_less.
 intro.
 eapply less_transitive_unfolded.
  2: apply (H0 H1).
 apply pos_div_two; assumption.
Qed.

Let Rolle_lemma13 :
  (forall (i : nat) (H : i <= n), fcp' _ H [<] [0])
  or (forall (i : nat) (H : i <= n), [0] [<] fcp' _ H) ->
  {x : IR | I x | forall Hx, AbsIR (F' x Hx) [<=] e}.
Proof.
 intro H; elim H; clear H; intro H0.
  exists (cp _ Hj).
   red in |- *; apply compact_part_hyp.
  intro; simpl in |- *; unfold ABSIR in |- *; apply Max_leEq.
   apply less_leEq; apply less_transitive_unfolded with ZeroR.
    eapply less_wdl.
     apply (H0 _ Hj).
    unfold fcp' in |- *; algebra.
   assumption.
  astepr ( [--][--]e); apply inv_resp_leEq.
  apply less_leEq; eapply less_wdr.
   apply Hj'.
  unfold fcp' in |- *; algebra.
 exists (cp _ Hk).
  red in |- *; apply compact_part_hyp.
 intros.
 simpl in |- *; unfold ABSIR in |- *; apply Max_leEq.
  apply less_leEq; eapply less_wdl.
   apply Hk'.
  unfold fcp' in |- *; algebra.
 apply less_leEq; apply less_transitive_unfolded with ZeroR.
  astepr ( [--]ZeroR); apply inv_resp_less; eapply less_wdr.
   apply (H0 _ Hk).
  unfold fcp' in |- *; rational.
 assumption.
Qed.

Let Rolle_lemma15 :
  (forall (i : nat) (H : i <= n), e [/]TwoNZ [<] AbsIR (fcp' _ H)) ->
  fcp' _ (Nat.le_0_l n) [<] [--] (e [/]TwoNZ) or e [/]TwoNZ [<] fcp' _ (Nat.le_0_l n).
Proof.
 intro H.
 cut (e [/]TwoNZ [<] fcp' _ (Nat.le_0_l n) or fcp' _ (Nat.le_0_l n) [<] [--] (e [/]TwoNZ)).
  intro H0; inversion_clear H0; [ right | left ]; assumption.
 apply less_AbsIR.
  apply pos_div_two; assumption.
 apply H.
Qed.
(* end hide *)

Theorem Rolle : {x : IR | I x | forall Hx, AbsIR (F' x Hx) [<=] e}.
Proof.
 elim Rolle_lemma9.
  exact Rolle_lemma10.
 intro.
 apply Rolle_lemma13.
 elim (Rolle_lemma15 b0).
  left; apply Rolle_lemma11.
   assumption.
  intro.
  eapply less_wdl.
   apply a0.
  unfold fcp' in |- *; algebra.
 right; apply Rolle_lemma12.
  assumption.
 intro.
 eapply less_wdr.
  apply b1.
 unfold fcp' in |- *; algebra.
Qed.

End Rolle.

Section Law_of_the_Mean.

(**
The following is a simple corollary:
*)

Variables a b : IR.
Hypothesis Hab' : a [<] b.

(* begin hide *)
Let Hab := less_leEq _ _ _ Hab'.
Let I := Compact Hab.
(* end hide *)

Variables F F' : PartIR.

Hypothesis HF : Derivative_I Hab' F F'.

(* begin show *)
Hypothesis HA : Dom F a.
Hypothesis HB : Dom F b.
(* end show *)

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.
 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.

End Law_of_the_Mean.

Section Corollaries.

(**
We can also state these theorems without expliciting the derivative of [F].
*)

Variables a b : IR.
Hypothesis Hab' : a [<] b.

(* begin hide *)
Let Hab := less_leEq _ _ _ Hab'.
(* end hide *)
Variable F : PartIR.

(* begin show *)
Hypothesis HF : Diffble_I Hab' F.
(* end show *)

Theorem Rolle' : (forall Ha Hb, F a Ha [=] F b Hb) -> forall e, [0] [<] e ->
 {x : IR | Compact Hab x | forall Hx, AbsIR (PartInt (ProjT1 HF) x Hx) [<=] e}.
Proof.
 intros.
 unfold Hab in |- *.
 apply Rolle with F (diffble_imp_inc _ _ _ _ HF _ (compact_inc_lft a b Hab))
   (diffble_imp_inc _ _ _ _ HF _ (compact_inc_rht a b Hab)).
   apply projT2.
  apply H.
 assumption.
Qed.

Lemma Law_of_the_Mean'_I : forall HA HB e, [0] [<] e ->
 {x : IR | Compact Hab x | forall Hx,
  AbsIR (F b HB[-]F a HA[-]PartInt (ProjT1 HF) x Hx[*] (b[-]a)) [<=] e}.
Proof.
 intros.
 unfold Hab in |- *.
 apply Law_of_the_Mean_I.
  apply projT2.
 assumption.
Qed.

End Corollaries.

Section Generalizations.

(**
The mean law is more useful if we abstract [a] and [b] from the
context---allowing them in particular to be equal.  In the case where
[F(a) [=] F(b)] we get Rolle's theorem again, so there is no need to
state it also in this form.

%\begin{convention}% Assume [I] is a proper interval, [F,F':PartIR].
%\end{convention}%
*)

Variable I : interval.
Hypothesis pI : proper I.

Variables F F' : PartIR.
(* begin show *)
Hypothesis derF : Derivative I pI F F'.
(* end show *)

(* begin hide *)
Let incF := Derivative_imp_inc _ _ _ _ derF.
Let incF' := Derivative_imp_inc' _ _ _ _ derF.
(* end hide *)

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.
 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.

(**
We further generalize the mean law by writing as an explicit bound.
*)

Theorem Law_of_the_Mean_Abs_ineq : forall a b, I a -> I b -> forall c,
 (forall x,  Compact (Min_leEq_Max a b) x -> forall Hx, AbsIR (F' x Hx) [<=] c) ->
 forall Ha Hb, AbsIR (F b Hb[-]F a Ha) [<=] c[*]AbsIR (b[-]a).
Proof.
 intros a b Ia Ib c Hc Ha Hb.
 astepr (c[*]AbsIR (b[-]a) [+][0]).
 apply shift_leEq_plus'.
 apply approach_zero_weak.
 intros e H.
 elim Law_of_the_Mean with a b e; auto.
 intros x H0 H1.
 cut (Dom F' x). intro H2.
  eapply leEq_transitive.
   2: apply (H1 Ha Hb H2).
  eapply leEq_transitive.
   2: apply triangle_IR_minus'.
  unfold cg_minus at 1 4 in |- *; apply plus_resp_leEq_lft.
  apply inv_resp_leEq.
  stepl (AbsIR (F' x H2)[*]AbsIR(b[-]a)).
   2:apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
  apply mult_resp_leEq_rht.
   auto.
  apply AbsIR_nonneg.
 apply (Derivative_imp_inc' _ _ _ _ derF).
 exact (included_interval I a b Ia Ib (Min_leEq_Max a b) x H0).
Qed.

Theorem Law_of_the_Mean_ineq : forall a b, I a -> I b -> forall c,
 (forall x,  Compact (Min_leEq_Max a b) x -> forall Hx, AbsIR (F' x Hx) [<=] c) ->
 forall Ha Hb, F b Hb[-]F a Ha [<=] c[*]AbsIR (b[-]a).
Proof.
 intros.
 eapply leEq_transitive.
  apply leEq_AbsIR.
 apply Law_of_the_Mean_Abs_ineq; assumption.
Qed.

End Generalizations.