From b528f4617a38ebf2b55645eb76a9a11407596471 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Thu, 16 Jan 2003 14:28:26 +0000
Subject: renommage de TAF.v en MVT.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3511 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 .depend.coq                |  12 +-
 Makefile                   |   2 +-
 theories/Reals/MVT.v       | 518 +++++++++++++++++++++++++++++++++++++++++++++
 theories/Reals/Ranalysis.v |   2 +-
 theories/Reals/Rpower.v    |   2 +-
 theories/Reals/TAF.v       | 518 ---------------------------------------------
 6 files changed, 527 insertions(+), 527 deletions(-)
 create mode 100644 theories/Reals/MVT.v
 delete mode 100644 theories/Reals/TAF.v

diff --git a/.depend.coq b/.depend.coq
index 076eb22739..5ca4168367 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -36,7 +36,7 @@ theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.v
 theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
 theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
 theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
+theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
 theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
 theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
 theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
@@ -46,8 +46,8 @@ theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase
 theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
 theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
 theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
+theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
 theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo
 theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo
 theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
@@ -219,7 +219,7 @@ theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.v
 theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
 theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
 theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
+theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
 theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
 theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
 theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
@@ -229,8 +229,8 @@ theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase
 theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
 theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
 theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
+theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
 theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo
 theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo
 theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
diff --git a/Makefile b/Makefile
index a1118adadf..fd2a14dbfb 100644
--- a/Makefile
+++ b/Makefile
@@ -580,7 +580,7 @@ REALS_all=theories/Reals/R_Ifp.vo \
 	theories/Reals/Rderiv.vo       theories/Reals/RList.vo \
 	theories/Reals/Ranalysis1.vo   theories/Reals/Ranalysis2.vo \
 	theories/Reals/Ranalysis3.vo   theories/Reals/Rtopology.vo \
-	theories/Reals/TAF.vo          theories/Reals/PSeries_reg.vo \
+	theories/Reals/MVT.vo          theories/Reals/PSeries_reg.vo \
 	theories/Reals/Exp_prop.vo     theories/Reals/Rtrigo_reg.vo \
 	theories/Reals/Rsqrt_def.vo    theories/Reals/R_sqrt.vo \
 	theories/Reals/Rtrigo_calc.vo  theories/Reals/Rgeom.vo \
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
new file mode 100644
index 0000000000..d797bb7d5d
--- /dev/null
+++ b/theories/Reals/MVT.v
@@ -0,0 +1,518 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+ 
+(*i $Id$ i*)
+
+Require Rbase.
+Require Rfunctions.
+Require Ranalysis1.
+Require Rtopology.
+
+(* Théorème des accroissements finis généralisés *)
+Theorem TAF_gen : (f,g:R->R;a,b:R;pr1:(c:R)``a<c<b``->(derivable_pt f c);pr2:(c:R)``a<c<b``->(derivable_pt g c)) ``a<b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> ((c:R)``a<=c<=b``->(continuity_pt g c)) -> (EXT c : R | (EXT P : ``a<c<b`` | ``((g b)-(g a))*(derive_pt f c (pr1 c P))==((f b)-(f a))*(derive_pt g c (pr2 c P))``)).
+Intros; Assert H2 := (Rlt_le ? ? H).
+Pose h := [y:R]``((g b)-(g a))*(f y)-((f b)-(f a))*(g y)``.
+Cut (c:R)``a<c<b``->(derivable_pt h c).
+Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt h c)).
+Intro; Assert H4 := (continuity_ab_maj h a b H2 H3).
+Assert H5 := (continuity_ab_min h a b H2 H3).
+Elim H4; Intros Mx H6.
+Elim H5; Intros mx H7.
+Cut (h a)==(h b).
+Intro; Pose M := (h Mx); Pose m := (h mx).
+Cut (c:R;P:``a<c<b``) (derive_pt h c (X c P))==``((g b)-(g a))*(derive_pt f c (pr1 c P))-((f b)-(f a))*(derive_pt g c (pr2 c P))``.
+Intro; Case (Req_EM (h a) M); Intro.
+Case (Req_EM (h a) m); Intro.
+Cut ((c:R)``a<=c<=b``->(h c)==M).
+Intro; Cut ``a<(a+b)/2<b``.
+(*** h constant ***)
+Intro; Exists ``(a+b)/2``.
+Exists H13.
+Apply Rminus_eq; Rewrite <- H9; Apply deriv_constant2 with a b.
+Elim H13; Intros; Assumption.
+Elim H13; Intros; Assumption.
+Intros; Rewrite (H12 ``(a+b)/2``).
+Apply H12; Split; Left; Assumption.
+Elim H13; Intros; Split; Left; Assumption.
+Split.
+Apply Rlt_monotony_contra with ``2``.
+Sup0.
+Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Apply H.
+DiscrR.
+Apply Rlt_monotony_contra with ``2``.
+Sup0.
+Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1l; Rewrite Rplus_sym; Rewrite double; Apply Rlt_compatibility; Apply H.
+DiscrR.
+Intros; Elim H6; Intros H13 _.
+Elim H7; Intros H14 _.
+Apply Rle_antisym.
+Apply H13; Apply H12.
+Rewrite H10 in H11; Rewrite H11; Apply H14; Apply H12.
+Cut ``a<mx<b``.
+(*** h admet un minimum global sur [a,b] ***)
+Intro; Exists mx.
+Exists H12.
+Apply Rminus_eq; Rewrite <- H9; Apply deriv_minimum with a b.
+Elim H12; Intros; Assumption.
+Elim H12; Intros; Assumption.
+Intros; Elim H7; Intros.
+Apply H15; Split; Left; Assumption.
+Elim H7; Intros _ H12; Elim H12; Intros; Split.
+Inversion H13.
+Apply H15.
+Rewrite H15 in H11; Elim H11; Reflexivity.
+Inversion H14.
+Apply H15.
+Rewrite H8 in H11; Rewrite <- H15 in H11; Elim H11; Reflexivity.
+Cut ``a<Mx<b``.
+(*** h admet un maximum global sur [a,b] ***)
+Intro; Exists Mx.
+Exists H11.
+Apply Rminus_eq; Rewrite <- H9; Apply deriv_maximum with a b.
+Elim H11; Intros; Assumption.
+Elim H11; Intros; Assumption.
+Intros; Elim H6; Intros; Apply H14.
+Split; Left; Assumption.
+Elim H6; Intros _ H11; Elim H11; Intros; Split.
+Inversion H12.
+Apply H14.
+Rewrite H14 in H10; Elim H10; Reflexivity.
+Inversion H13.
+Apply H14.
+Rewrite H8 in H10; Rewrite <- H14 in H10; Elim H10; Reflexivity.
+Intros; Unfold h; Replace (derive_pt [y:R]``((g b)-(g a))*(f y)-((f b)-(f a))*(g y)`` c (X c P)) with (derive_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c (derivable_pt_minus ? ? ? (derivable_pt_mult ? ? ? (derivable_pt_const ``(g b)-(g a)`` c) (pr1 c P)) (derivable_pt_mult ? ? ? (derivable_pt_const ``(f b)-(f a)`` c) (pr2 c P)))); [Idtac | Apply pr_nu].
+Rewrite derive_pt_minus; Do 2 Rewrite derive_pt_mult; Do 2 Rewrite derive_pt_const; Do 2 Rewrite Rmult_Ol; Do 2 Rewrite Rplus_Ol; Reflexivity.
+Unfold h; Ring.
+Intros; Unfold h; Change (continuity_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c).
+Apply continuity_pt_minus; Apply continuity_pt_mult.
+Apply derivable_continuous_pt; Apply derivable_const.
+Apply H0; Apply H3.
+Apply derivable_continuous_pt; Apply derivable_const.
+Apply H1; Apply H3.
+Intros; Change (derivable_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c).
+Apply derivable_pt_minus; Apply derivable_pt_mult.
+Apply derivable_pt_const.
+Apply (pr1 ? H3).
+Apply derivable_pt_const.
+Apply (pr2 ? H3).
+Qed.
+
+(* Une version plus faible (mais usuelle ) *)
+Lemma TAF : (f:(R->R); a,b:R; pr:(derivable f)) ``a < b``->(EXT c:R | ``(f b)-(f a) == (derive_pt f c (pr c))*(b-a)``/\``a < c < b``).
+Intros; Cut (c:R)``a<c<b``->(derivable_pt f c); [Intro | Intros; Apply pr].
+Cut (c:R)``a<c<b``->(derivable_pt id c); [Intro | Intros; Apply derivable_pt_id].
+Cut ((c:R)``a<=c<=b``->(continuity_pt f c)); [Intro | Intros; Apply derivable_continuous_pt; Apply pr].
+Cut ((c:R)``a<=c<=b``->(continuity_pt id c)); [Intro | Intros; Apply derivable_continuous_pt; Apply derivable_id].
+Assert H2 := (TAF_gen f id a b X X0 H H0 H1).
+Elim H2; Intros c H3; Elim H3; Intros.
+Exists c; Split.
+Cut (derive_pt id c (X0 c x)) == (derive_pt id c (derivable_pt_id c)); [Intro | Apply pr_nu].
+Rewrite H5 in H4; Rewrite (derive_pt_id c) in H4; Rewrite Rmult_1r in H4; Rewrite <- H4; Replace (derive_pt f c (X c x)) with (derive_pt f c (pr c)); [Idtac | Apply pr_nu]; Apply Rmult_sym.
+Apply x.
+Qed.
+
+Theorem TAF_cor1 : (f,f':R->R;a,b:R) ``a<b`` -> ((c:R)``a<=c<=b``->(derivable_pt_lim f c (f' c))) -> (EXT c:R | ``(f b)-(f a)==(f' c)*(b-a)``/\``a<c<b``).
+Intros; Cut ((c:R)``a<=c<=b``->(derivable_pt f c)).
+Intro; Cut ((c:R)``a<c<b``->(derivable_pt f c)).
+Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt f c)).
+Intro; Cut ((c:R)``a<=c<=b``->(derivable_pt id c)).
+Intro; Cut ((c:R)``a<c<b``->(derivable_pt id c)).
+Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt id c)).
+Intro; Elim (TAF_gen f id a b X0 X2 H H1 H2); Intros; Elim H3; Clear H3; Intros; Exists x; Split.
+Cut (derive_pt id x (X2 x x0))==R1.
+Cut (derive_pt f x (X0 x x0))==(f' x).
+Intros; Rewrite H4 in H3; Rewrite H5 in H3; Unfold id in H3; Rewrite Rmult_1r in H3; Rewrite Rmult_sym; Symmetry; Assumption.
+Apply derive_pt_eq_0; Apply H0; Elim x0; Intros; Split; Left; Assumption.
+Apply derive_pt_eq_0; Apply derivable_pt_lim_id.
+Assumption.
+Intros; Apply derivable_continuous_pt; Apply X1; Assumption.
+Intros; Apply derivable_pt_id.
+Intros; Apply derivable_pt_id.
+Intros; Apply derivable_continuous_pt; Apply X; Assumption.
+Intros; Elim H1; Intros; Apply X; Split; Left; Assumption.
+Intros; Unfold derivable_pt; Apply Specif.existT with (f' c); Apply H0; Apply H1.
+Qed.
+
+Lemma TAF_cor2 : (f,f':(R->R); a,b:R) ``a < b``  -> ((x:R)``a <= x`` ->  ``x <= b``->(derivable_pt_lim f x (f' x))) -> (EXT c:R | ``a<=c``/\``c<=b``/\``(f b)==(f a) + (f' c)*(b-a)``).
+Intros; Assert H1 : (EXT c:R | ``(f b) -(f a) == (f' c)*(b-a)``/\``a<c<b``); [Apply TAF_cor1; [Apply H | Intros; Elim H1; Intros; Apply (H0 ? H2 H3)] | Elim H1; Intros; Exists x; Elim H2; Intros; Elim H4; Intros; Split; [Left; Assumption | Split; [Left; Assumption | Rewrite <- H3; Ring]]].
+Qed.
+
+(*** Corollaires ***)
+
+Lemma Rolle : (f:R->R;a,b:R;pr:(x:R)``a<x<b``->(derivable_pt f x)) ((x:R)``a<=x<=b``->(continuity_pt f x)) -> ``a<b`` -> (f a)==(f b) -> (EXT c:R | (EXT P: ``a<c<b`` | ``(derive_pt f c (pr c P))==0``)).
+Intros; Assert H2 : (x:R)``a<x<b``->(derivable_pt id x).
+Intros; Apply derivable_pt_id.
+Assert H3 := (TAF_gen f id a b pr H2 H0 H); Assert H4 : (x:R)``a<=x<=b``->(continuity_pt id x).
+Intros; Apply derivable_continuous; Apply derivable_id.
+Elim (H3 H4); Intros; Elim H5; Intros; Exists x; Exists x0; Rewrite H1 in H6; Unfold id in H6; Unfold Rminus in H6; Rewrite Rplus_Ropp_r in H6; Rewrite Rmult_Ol in H6; Apply r_Rmult_mult with ``b-a``; [Rewrite Rmult_Or; Apply H6 | Apply Rminus_eq_contra; Red; Intro; Rewrite H7 in H0; Elim (Rlt_antirefl ? H0)].
+Qed.
+
+(**********)
+Lemma nonneg_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``0<=(derive_pt f x (pr x))``) -> (increasing f).
+Intros.
+Unfold increasing.
+Intros.
+Case (total_order_T x y); Intro.
+Elim s; Intro.
+Apply Rle_anti_compatibility with ``-(f x)``.
+Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
+Assert H1 := (TAF f ? ? pr a).
+Elim H1; Intros.
+Elim H2; Intros.
+Unfold Rminus in H3.
+Rewrite H3.
+Apply Rmult_le_pos.
+Apply H.
+Apply Rle_anti_compatibility with x.
+Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring].
+Rewrite b; Right; Reflexivity.
+Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H0 r)).
+Qed.
+ 
+(**********)
+Lemma nonpos_derivative_0 : (f:R->R;pr:(derivable f)) (decreasing f) -> ((x:R) ``(derive_pt f x (pr x))<=0``).
+Intros; Assert H0 :=H; Unfold decreasing in H0; Generalize (derivable_derive f x (pr x)); Intro; Elim H1; Intros l H2.
+Rewrite H2; Case (total_order l R0); Intro.
+Left; Assumption.
+Elim H3; Intro.
+Right; Assumption.
+Generalize (derive_pt_eq_1 f x l (pr x) H2); Intros; Cut ``0< (l/2)``.
+Intro; Elim (H5 ``(l/2)`` H6); Intros delta H7; Cut ``delta/2<>0``/\``0<delta/2``/\``(Rabsolu delta/2)<delta``.
+Intro; Decompose [and] H8; Intros; Generalize (H7 ``delta/2`` H9 H12); Cut ``((f (x+delta/2))-(f x))/(delta/2)<=0``.
+Intro; Cut ``0< -(((f (x+delta/2))-(f x))/(delta/2)-l)``.
+Intro; Unfold Rabsolu; Case (case_Rabsolu ``((f (x+delta/2))-(f x))/(delta/2)-l``).
+Intros; Generalize (Rlt_compatibility_r ``-l`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``(l/2)`` H14); Unfold Rminus.
+Replace ``(l/2)+ -l`` with ``-(l/2)``.
+Replace `` -(((f (x+delta/2))+ -(f x))/(delta/2)+ -l)+ -l`` with ``-(((f (x+delta/2))+ -(f x))/(delta/2))``.
+Intro.
+Generalize (Rlt_Ropp ``-(((f (x+delta/2))+ -(f x))/(delta/2))`` ``-(l/2)`` H15). 
+Repeat Rewrite Ropp_Ropp.
+Intro.
+Generalize (Rlt_trans ``0`` ``l/2`` ``((f (x+delta/2))-(f x))/(delta/2)`` H6 H16); Intro.
+Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``0`` H17 H10)).
+Ring.
+Pattern 3 l; Rewrite double_var.
+Ring.
+Intros.
+Generalize (Rge_Ropp ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` r).
+Rewrite Ropp_O.
+Intro.
+Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``0`` H13 H15)).
+Replace ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` with ``(((f (x))-(f (x+delta/2)))/(delta/2)) +l``.
+Unfold Rminus.
+Apply ge0_plus_gt0_is_gt0.
+Unfold Rdiv; Apply Rmult_le_pos.
+Cut ``x<=(x+(delta*/2))``.
+Intro; Generalize (H0 x ``x+(delta*/2)`` H13); Intro; Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H14); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption.
+Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption.
+Left; Apply Rlt_Rinv; Assumption.
+Assumption.
+Rewrite Ropp_distr2.
+Unfold Rminus.
+Rewrite (Rplus_sym l).
+Unfold Rdiv.
+Rewrite <- Ropp_mul1.
+Rewrite Ropp_distr1.
+Rewrite Ropp_Ropp.
+Rewrite (Rplus_sym (f x)).
+Reflexivity.
+Replace ``((f (x+delta/2))-(f x))/(delta/2)`` with ``-(((f x)-(f (x+delta/2)))/(delta/2))``.
+Rewrite <- Ropp_O.
+Apply Rge_Ropp.
+Apply Rle_sym1.
+Unfold Rdiv; Apply Rmult_le_pos.
+Cut ``x<=(x+(delta*/2))``.
+Intro; Generalize (H0 x ``x+(delta*/2)`` H10); Intro.
+Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H13); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption.
+Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption.
+Left; Apply Rlt_Rinv; Assumption.
+Unfold Rdiv; Rewrite <- Ropp_mul1.
+Rewrite Ropp_distr2.
+Reflexivity.
+Split.
+Unfold Rdiv; Apply prod_neq_R0.
+Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H8; Elim (Rlt_antirefl ``0`` H8).
+Apply Rinv_neq_R0; DiscrR.
+Split.
+Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Sup0].
+Rewrite Rabsolu_right.
+Unfold Rdiv; Apply Rlt_monotony_contra with ``2``.
+Sup0.
+Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1l; Rewrite double; Pattern 1 (pos delta); Rewrite <- Rplus_Or.
+Apply Rlt_compatibility; Apply (cond_pos delta).
+DiscrR.
+Apply Rle_sym1; Unfold Rdiv; Left; Apply Rmult_lt_pos.
+Apply (cond_pos delta).
+Apply Rlt_Rinv; Sup0.
+Unfold Rdiv; Apply Rmult_lt_pos; [Apply H4 | Apply Rlt_Rinv; Sup0].
+Qed.
+
+(**********)
+Lemma increasing_decreasing_opp : (f:R->R) (increasing f) -> (decreasing (opp_fct f)).
+Unfold increasing decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rge_Ropp; Apply Rle_sym1; Assumption.
+Qed.
+
+(**********)
+Lemma nonpos_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<=0``) -> (decreasing f).
+Intros.
+Cut (h:R)``-(-(f h))==(f h)``.
+Intro.
+Generalize (increasing_decreasing_opp (opp_fct f)).
+Unfold decreasing.
+Unfold opp_fct.
+Intros.
+Rewrite <- (H0 x); Rewrite <- (H0 y).
+Apply H1.
+Cut (x:R)``0<=(derive_pt (opp_fct f) x ((derivable_opp f pr) x))``.
+Intros.
+Replace [x:R]``-(f x)`` with (opp_fct f); [Idtac | Reflexivity].
+Apply (nonneg_derivative_1 (opp_fct f) (derivable_opp f pr) H3).
+Intro.
+Assert H3 := (derive_pt_opp f x0 (pr x0)).
+Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``.
+Intro.
+Rewrite <- H4.
+Rewrite H3.
+Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H x0).
+Apply pr_nu.
+Assumption.
+Intro; Ring.
+Qed.
+ 
+(**********)
+Lemma positive_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``0<(derive_pt f x (pr x))``)->(strict_increasing f).
+Intros.
+Unfold strict_increasing.
+Intros.
+Apply Rlt_anti_compatibility with ``-(f x)``.
+Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
+Assert H1 := (TAF f ? ? pr H0).
+Elim H1; Intros.
+Elim H2; Intros.
+Unfold Rminus in H3.
+Rewrite H3.
+Apply Rmult_lt_pos.
+Apply H.
+Apply Rlt_anti_compatibility with x.
+Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring].
+Qed.
+
+(**********)
+Lemma strictincreasing_strictdecreasing_opp : (f:R->R) (strict_increasing f) ->
+(strict_decreasing (opp_fct f)).
+Unfold strict_increasing strict_decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rlt_Ropp; Assumption.
+Qed.
+ 
+(**********)
+Lemma negative_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<0``)->(strict_decreasing f).
+Intros.
+Cut (h:R)``- (-(f h))==(f h)``.
+Intros.
+Generalize (strictincreasing_strictdecreasing_opp (opp_fct f)).
+Unfold strict_decreasing opp_fct.
+Intros.
+Rewrite <- (H0 x).
+Rewrite <- (H0 y).
+Apply H1; [Idtac | Assumption].
+Cut (x:R)``0<(derive_pt (opp_fct f) x (derivable_opp f pr x))``.
+Intros; EApply positive_derivative; Apply H3.
+Intro.
+Assert H3 := (derive_pt_opp f x0 (pr x0)).
+Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``.
+Intro.
+Rewrite <- H4; Rewrite H3.
+Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H x0).
+Apply pr_nu.
+Intro; Ring.
+Qed.
+ 
+(**********)
+Lemma null_derivative_0 : (f:R->R;pr:(derivable f)) (constant f)->((x:R) ``(derive_pt f x (pr x))==0``). 
+Intros.
+Unfold constant in H.
+Apply derive_pt_eq_0.
+Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Simpl; Intros.
+Rewrite (H x ``x+h``); Unfold Rminus; Unfold Rdiv; Rewrite Rplus_Ropp_r; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
+Qed.
+
+(**********)
+Lemma increasing_decreasing : (f:R->R) (increasing f) -> (decreasing f) -> (constant f).
+Unfold increasing decreasing constant; Intros; Case (total_order x y); Intro.
+Generalize (Rlt_le x y H1); Intro; Apply (Rle_antisym (f x) (f y) (H x y H2) (H0 x y H2)).
+Elim H1; Intro.
+Rewrite H2; Reflexivity.
+Generalize (Rlt_le y x H2); Intro; Symmetry; Apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)).
+Qed.
+
+(**********)
+Lemma null_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))==0``)->(constant f).
+Intros.
+Cut (x:R)``(derive_pt f x (pr x)) <= 0``.
+Cut (x:R)``0 <= (derive_pt f x (pr x))``.
+Intros.
+Assert H2 := (nonneg_derivative_1 f pr H0).
+Assert H3 := (nonpos_derivative_1 f  pr H1).
+Apply increasing_decreasing; Assumption.
+Intro; Right; Symmetry; Apply (H x).
+Intro; Right; Apply (H x).
+Qed.
+
+(**********)
+Lemma derive_increasing_interv_ax : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> (((t:R) ``a<t<b`` -> ``0<(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``)) /\ (((t:R) ``a<t<b`` -> ``0<=(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``)).
+Intros.
+Split; Intros.
+Apply Rlt_anti_compatibility with ``-(f x)``.
+Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
+Assert H4 := (TAF f ? ? pr H3).
+Elim H4; Intros.
+Elim H5; Intros.
+Unfold Rminus in H6.
+Rewrite H6.
+Apply Rmult_lt_pos.
+Apply H0.
+Elim H7; Intros.
+Split.
+Elim H1; Intros.
+Apply Rle_lt_trans with x; Assumption.
+Elim H2; Intros.
+Apply Rlt_le_trans with y; Assumption.
+Apply Rlt_anti_compatibility with x.
+Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring].
+Apply Rle_anti_compatibility with ``-(f x)``.
+Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
+Assert H4 := (TAF f ? ? pr H3).
+Elim H4; Intros.
+Elim H5; Intros.
+Unfold Rminus in H6.
+Rewrite H6.
+Apply Rmult_le_pos.
+Apply H0.
+Elim H7; Intros.
+Split.
+Elim H1; Intros.
+Apply Rle_lt_trans with x; Assumption.
+Elim H2; Intros.
+Apply Rlt_le_trans with y; Assumption.
+Apply Rle_anti_compatibility with x.
+Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Left; Assumption | Ring].
+Qed.
+
+(**********)
+Lemma derive_increasing_interv : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``).
+Intros.
+Generalize (derive_increasing_interv_ax a b f pr H); Intro.
+Elim H4; Intros H5 _; Apply (H5 H0 x y H1 H2 H3).
+Qed.
+
+(**********)
+Lemma derive_increasing_interv_var : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<=(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``).
+Intros; Generalize (derive_increasing_interv_ax a b f pr H); Intro; Elim H4; Intros _ H5; Apply (H5 H0 x y H1 H2 H3).
+Qed.
+
+(**********)
+(**********)
+Theorem IAF : (f:R->R;a,b,k:R;pr:(derivable f)) ``a<=b`` -> ((c:R) ``a<=c<=b`` -> ``(derive_pt f c (pr c))<=k``) -> ``(f b)-(f a)<=k*(b-a)``.
+Intros.
+Case (total_order_T a b); Intro.
+Elim s; Intro.
+Assert H1 := (TAF f ? ? pr a0).
+Elim H1; Intros.
+Elim H2; Intros.
+Rewrite H3.
+Do 2 Rewrite <- (Rmult_sym ``(b-a)``).
+Apply Rle_monotony.
+Apply Rle_anti_compatibility with ``a``; Rewrite Rplus_Or.
+Replace ``a+(b-a)`` with b; [Assumption | Ring].
+Apply H0.
+Elim H4; Intros.
+Split; Left; Assumption.
+Rewrite b0.
+Unfold Rminus; Do 2 Rewrite Rplus_Ropp_r.
+Rewrite Rmult_Or; Right; Reflexivity.
+Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)).
+Qed.
+
+Lemma IAF_var : (f,g:R->R;a,b:R;pr1:(derivable f);pr2:(derivable g)) ``a<=b`` -> ((c:R) ``a<=c<=b`` -> ``(derive_pt g c (pr2 c))<=(derive_pt f c (pr1 c))``) -> ``(g b)-(g a)<=(f b)-(f a)``.
+Intros.
+Cut (derivable (minus_fct g f)).
+Intro.
+Cut (c:R)``a<=c<=b``->``(derive_pt (minus_fct g f) c (X c))<=0``.
+Intro. 
+Assert H2 := (IAF (minus_fct g f) a b R0 X H H1).
+Rewrite Rmult_Ol in H2; Unfold minus_fct in H2.
+Apply Rle_anti_compatibility with ``-(f b)+(f a)``.
+Replace ``-(f b)+(f a)+((f b)-(f a))`` with R0; [Idtac | Ring].
+Replace ``-(f b)+(f a)+((g b)-(g a))`` with ``(g b)-(f b)-((g a)-(f a))``; [Apply H2 | Ring].
+Intros.
+Cut (derive_pt (minus_fct g f) c (X c))==(derive_pt (minus_fct g f) c (derivable_pt_minus ? ? ? (pr2 c) (pr1 c))).
+Intro.
+Rewrite H2.
+Rewrite derive_pt_minus.
+Apply Rle_anti_compatibility with (derive_pt f c (pr1 c)).
+Rewrite Rplus_Or.
+Replace ``(derive_pt f c (pr1 c))+((derive_pt g c (pr2 c))-(derive_pt f c (pr1 c)))`` with ``(derive_pt g c (pr2 c))``; [Idtac | Ring].
+Apply H0; Assumption.
+Apply pr_nu.
+Apply derivable_minus; Assumption.
+Qed.
+
+(* If f has a null derivative in ]a,b[ and is continue in [a,b], *)
+(* then f is constant on [a,b] *)
+Lemma null_derivative_loc : (f:R->R;a,b:R;pr:(x:R)``a<x<b``->(derivable_pt f x)) ((x:R)``a<=x<=b``->(continuity_pt f x)) -> ((x:R;P:``a<x<b``)(derive_pt f x (pr x P))==R0) -> (constant_D_eq f [x:R]``a<=x<=b`` (f a)).
+Intros; Unfold constant_D_eq; Intros; Case (total_order_T a b); Intro.
+Elim s; Intro.
+Assert H2 : (y:R)``a<y<x``->(derivable_pt id y).
+Intros; Apply derivable_pt_id.
+Assert H3 : (y:R)``a<=y<=x``->(continuity_pt id y).
+Intros; Apply derivable_continuous; Apply derivable_id.
+Assert H4 : (y:R)``a<y<x``->(derivable_pt f y).
+Intros; Apply pr; Elim H4; Intros; Split.
+Assumption.
+Elim H1; Intros; Apply Rlt_le_trans with x; Assumption.
+Assert H5 : (y:R)``a<=y<=x``->(continuity_pt f y).
+Intros; Apply H; Elim H5; Intros; Split.
+Assumption.
+Elim H1; Intros; Apply Rle_trans with x; Assumption.
+Elim H1; Clear H1; Intros; Elim H1; Clear H1; Intro.
+Assert H7 := (TAF_gen f id a x H4 H2 H1 H5 H3).
+Elim H7; Intros; Elim H8; Intros; Assert H10 : ``a<x0<b``.
+Elim x1; Intros; Split.
+Assumption.
+Apply Rlt_le_trans with x; Assumption.
+Assert H11 : ``(derive_pt f x0 (H4 x0 x1))==0``.
+Replace (derive_pt f x0 (H4 x0 x1)) with (derive_pt f x0 (pr x0 H10)); [Apply H0 | Apply pr_nu].
+Assert H12 : ``(derive_pt id x0 (H2 x0 x1))==1``.
+Apply derive_pt_eq_0; Apply derivable_pt_lim_id.
+Rewrite H11 in H9; Rewrite H12 in H9; Rewrite Rmult_Or in H9; Rewrite Rmult_1r in H9; Apply Rminus_eq; Symmetry; Assumption.
+Rewrite H1; Reflexivity.
+Assert H2 : x==a.
+Rewrite <- b0 in H1; Elim H1; Intros; Apply Rle_antisym; Assumption.
+Rewrite H2; Reflexivity.
+Elim H1; Intros; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? (Rle_trans ? ? ? H2 H3) r)).
+Qed.
+
+(* La primitive est unique a une constante pres *)
+Lemma antiderivative_Ucte : (f,g1,g2:R->R;a,b:R) (antiderivative f g1 a b) -> (antiderivative f g2 a b) -> (EXT c:R | (x:R)``a<=x<=b``->``(g1 x)==(g2 x)+c``).
+Unfold antiderivative; Intros; Elim H; Clear H; Intros; Elim H0; Clear H0; Intros H0 _; Exists ``(g1 a)-(g2 a)``; Intros; Assert H3 : (x:R)``a<=x<=b``->(derivable_pt g1 x).
+Intros; Unfold derivable_pt; Apply Specif.existT with (f x0); Elim (H x0 H3); Intros; EApply derive_pt_eq_1; Symmetry; Apply H4.
+Assert H4 : (x:R)``a<=x<=b``->(derivable_pt g2 x).
+Intros; Unfold derivable_pt; Apply Specif.existT with (f x0); Elim (H0 x0 H4); Intros; EApply derive_pt_eq_1; Symmetry; Apply H5.
+Assert H5 : (x:R)``a<x<b``->(derivable_pt (minus_fct g1 g2) x).
+Intros; Elim H5; Intros; Apply derivable_pt_minus; [Apply H3; Split; Left; Assumption | Apply H4; Split; Left; Assumption].
+Assert H6 : (x:R)``a<=x<=b``->(continuity_pt (minus_fct g1 g2) x).
+Intros; Apply derivable_continuous_pt; Apply derivable_pt_minus; [Apply H3 | Apply H4]; Assumption.
+Assert H7 : (x:R;P:``a<x<b``)(derive_pt (minus_fct g1 g2) x (H5 x P))==``0``.
+Intros; Elim P; Intros; Apply derive_pt_eq_0; Replace R0 with ``(f x0)-(f x0)``; [Idtac | Ring].
+Assert H9 : ``a<=x0<=b``.
+Split; Left; Assumption.
+Apply derivable_pt_lim_minus; [Elim (H ? H9) | Elim (H0 ? H9)]; Intros; EApply derive_pt_eq_1; Symmetry; Apply H10.
+Assert H8 := (null_derivative_loc (minus_fct g1 g2) a b H5 H6 H7); Unfold constant_D_eq in H8; Assert H9 := (H8 ? H2); Unfold minus_fct in H9; Rewrite <- H9; Ring.
+Qed.
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index ec2cd0c464..c56a90dc76 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -16,7 +16,7 @@ Require Export Ranalysis1.
 Require Export Ranalysis2.
 Require Export Ranalysis3.
 Require Export Rtopology.
-Require Export TAF.
+Require Export MVT.
 Require Export PSeries_reg.
 Require Export Exp_prop.
 Require Export Rtrigo_reg.
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index c52c98289a..5de89f939b 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -22,7 +22,7 @@ Require Ranalysis1.
 Require Exp_prop.
 Require Rsqrt_def.
 Require R_sqrt.
-Require TAF.
+Require MVT.
 Require Ranalysis4.
 
 Lemma P_Rmin: (P : R ->  Prop) (x, y : R) (P x) -> (P y) ->  (P (Rmin x y)).
diff --git a/theories/Reals/TAF.v b/theories/Reals/TAF.v
deleted file mode 100644
index d797bb7d5d..0000000000
--- a/theories/Reals/TAF.v
+++ /dev/null
@@ -1,518 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
- 
-(*i $Id$ i*)
-
-Require Rbase.
-Require Rfunctions.
-Require Ranalysis1.
-Require Rtopology.
-
-(* Théorème des accroissements finis généralisés *)
-Theorem TAF_gen : (f,g:R->R;a,b:R;pr1:(c:R)``a<c<b``->(derivable_pt f c);pr2:(c:R)``a<c<b``->(derivable_pt g c)) ``a<b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> ((c:R)``a<=c<=b``->(continuity_pt g c)) -> (EXT c : R | (EXT P : ``a<c<b`` | ``((g b)-(g a))*(derive_pt f c (pr1 c P))==((f b)-(f a))*(derive_pt g c (pr2 c P))``)).
-Intros; Assert H2 := (Rlt_le ? ? H).
-Pose h := [y:R]``((g b)-(g a))*(f y)-((f b)-(f a))*(g y)``.
-Cut (c:R)``a<c<b``->(derivable_pt h c).
-Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt h c)).
-Intro; Assert H4 := (continuity_ab_maj h a b H2 H3).
-Assert H5 := (continuity_ab_min h a b H2 H3).
-Elim H4; Intros Mx H6.
-Elim H5; Intros mx H7.
-Cut (h a)==(h b).
-Intro; Pose M := (h Mx); Pose m := (h mx).
-Cut (c:R;P:``a<c<b``) (derive_pt h c (X c P))==``((g b)-(g a))*(derive_pt f c (pr1 c P))-((f b)-(f a))*(derive_pt g c (pr2 c P))``.
-Intro; Case (Req_EM (h a) M); Intro.
-Case (Req_EM (h a) m); Intro.
-Cut ((c:R)``a<=c<=b``->(h c)==M).
-Intro; Cut ``a<(a+b)/2<b``.
-(*** h constant ***)
-Intro; Exists ``(a+b)/2``.
-Exists H13.
-Apply Rminus_eq; Rewrite <- H9; Apply deriv_constant2 with a b.
-Elim H13; Intros; Assumption.
-Elim H13; Intros; Assumption.
-Intros; Rewrite (H12 ``(a+b)/2``).
-Apply H12; Split; Left; Assumption.
-Elim H13; Intros; Split; Left; Assumption.
-Split.
-Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Apply H.
-DiscrR.
-Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l; Rewrite Rplus_sym; Rewrite double; Apply Rlt_compatibility; Apply H.
-DiscrR.
-Intros; Elim H6; Intros H13 _.
-Elim H7; Intros H14 _.
-Apply Rle_antisym.
-Apply H13; Apply H12.
-Rewrite H10 in H11; Rewrite H11; Apply H14; Apply H12.
-Cut ``a<mx<b``.
-(*** h admet un minimum global sur [a,b] ***)
-Intro; Exists mx.
-Exists H12.
-Apply Rminus_eq; Rewrite <- H9; Apply deriv_minimum with a b.
-Elim H12; Intros; Assumption.
-Elim H12; Intros; Assumption.
-Intros; Elim H7; Intros.
-Apply H15; Split; Left; Assumption.
-Elim H7; Intros _ H12; Elim H12; Intros; Split.
-Inversion H13.
-Apply H15.
-Rewrite H15 in H11; Elim H11; Reflexivity.
-Inversion H14.
-Apply H15.
-Rewrite H8 in H11; Rewrite <- H15 in H11; Elim H11; Reflexivity.
-Cut ``a<Mx<b``.
-(*** h admet un maximum global sur [a,b] ***)
-Intro; Exists Mx.
-Exists H11.
-Apply Rminus_eq; Rewrite <- H9; Apply deriv_maximum with a b.
-Elim H11; Intros; Assumption.
-Elim H11; Intros; Assumption.
-Intros; Elim H6; Intros; Apply H14.
-Split; Left; Assumption.
-Elim H6; Intros _ H11; Elim H11; Intros; Split.
-Inversion H12.
-Apply H14.
-Rewrite H14 in H10; Elim H10; Reflexivity.
-Inversion H13.
-Apply H14.
-Rewrite H8 in H10; Rewrite <- H14 in H10; Elim H10; Reflexivity.
-Intros; Unfold h; Replace (derive_pt [y:R]``((g b)-(g a))*(f y)-((f b)-(f a))*(g y)`` c (X c P)) with (derive_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c (derivable_pt_minus ? ? ? (derivable_pt_mult ? ? ? (derivable_pt_const ``(g b)-(g a)`` c) (pr1 c P)) (derivable_pt_mult ? ? ? (derivable_pt_const ``(f b)-(f a)`` c) (pr2 c P)))); [Idtac | Apply pr_nu].
-Rewrite derive_pt_minus; Do 2 Rewrite derive_pt_mult; Do 2 Rewrite derive_pt_const; Do 2 Rewrite Rmult_Ol; Do 2 Rewrite Rplus_Ol; Reflexivity.
-Unfold h; Ring.
-Intros; Unfold h; Change (continuity_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c).
-Apply continuity_pt_minus; Apply continuity_pt_mult.
-Apply derivable_continuous_pt; Apply derivable_const.
-Apply H0; Apply H3.
-Apply derivable_continuous_pt; Apply derivable_const.
-Apply H1; Apply H3.
-Intros; Change (derivable_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c).
-Apply derivable_pt_minus; Apply derivable_pt_mult.
-Apply derivable_pt_const.
-Apply (pr1 ? H3).
-Apply derivable_pt_const.
-Apply (pr2 ? H3).
-Qed.
-
-(* Une version plus faible (mais usuelle ) *)
-Lemma TAF : (f:(R->R); a,b:R; pr:(derivable f)) ``a < b``->(EXT c:R | ``(f b)-(f a) == (derive_pt f c (pr c))*(b-a)``/\``a < c < b``).
-Intros; Cut (c:R)``a<c<b``->(derivable_pt f c); [Intro | Intros; Apply pr].
-Cut (c:R)``a<c<b``->(derivable_pt id c); [Intro | Intros; Apply derivable_pt_id].
-Cut ((c:R)``a<=c<=b``->(continuity_pt f c)); [Intro | Intros; Apply derivable_continuous_pt; Apply pr].
-Cut ((c:R)``a<=c<=b``->(continuity_pt id c)); [Intro | Intros; Apply derivable_continuous_pt; Apply derivable_id].
-Assert H2 := (TAF_gen f id a b X X0 H H0 H1).
-Elim H2; Intros c H3; Elim H3; Intros.
-Exists c; Split.
-Cut (derive_pt id c (X0 c x)) == (derive_pt id c (derivable_pt_id c)); [Intro | Apply pr_nu].
-Rewrite H5 in H4; Rewrite (derive_pt_id c) in H4; Rewrite Rmult_1r in H4; Rewrite <- H4; Replace (derive_pt f c (X c x)) with (derive_pt f c (pr c)); [Idtac | Apply pr_nu]; Apply Rmult_sym.
-Apply x.
-Qed.
-
-Theorem TAF_cor1 : (f,f':R->R;a,b:R) ``a<b`` -> ((c:R)``a<=c<=b``->(derivable_pt_lim f c (f' c))) -> (EXT c:R | ``(f b)-(f a)==(f' c)*(b-a)``/\``a<c<b``).
-Intros; Cut ((c:R)``a<=c<=b``->(derivable_pt f c)).
-Intro; Cut ((c:R)``a<c<b``->(derivable_pt f c)).
-Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt f c)).
-Intro; Cut ((c:R)``a<=c<=b``->(derivable_pt id c)).
-Intro; Cut ((c:R)``a<c<b``->(derivable_pt id c)).
-Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt id c)).
-Intro; Elim (TAF_gen f id a b X0 X2 H H1 H2); Intros; Elim H3; Clear H3; Intros; Exists x; Split.
-Cut (derive_pt id x (X2 x x0))==R1.
-Cut (derive_pt f x (X0 x x0))==(f' x).
-Intros; Rewrite H4 in H3; Rewrite H5 in H3; Unfold id in H3; Rewrite Rmult_1r in H3; Rewrite Rmult_sym; Symmetry; Assumption.
-Apply derive_pt_eq_0; Apply H0; Elim x0; Intros; Split; Left; Assumption.
-Apply derive_pt_eq_0; Apply derivable_pt_lim_id.
-Assumption.
-Intros; Apply derivable_continuous_pt; Apply X1; Assumption.
-Intros; Apply derivable_pt_id.
-Intros; Apply derivable_pt_id.
-Intros; Apply derivable_continuous_pt; Apply X; Assumption.
-Intros; Elim H1; Intros; Apply X; Split; Left; Assumption.
-Intros; Unfold derivable_pt; Apply Specif.existT with (f' c); Apply H0; Apply H1.
-Qed.
-
-Lemma TAF_cor2 : (f,f':(R->R); a,b:R) ``a < b``  -> ((x:R)``a <= x`` ->  ``x <= b``->(derivable_pt_lim f x (f' x))) -> (EXT c:R | ``a<=c``/\``c<=b``/\``(f b)==(f a) + (f' c)*(b-a)``).
-Intros; Assert H1 : (EXT c:R | ``(f b) -(f a) == (f' c)*(b-a)``/\``a<c<b``); [Apply TAF_cor1; [Apply H | Intros; Elim H1; Intros; Apply (H0 ? H2 H3)] | Elim H1; Intros; Exists x; Elim H2; Intros; Elim H4; Intros; Split; [Left; Assumption | Split; [Left; Assumption | Rewrite <- H3; Ring]]].
-Qed.
-
-(*** Corollaires ***)
-
-Lemma Rolle : (f:R->R;a,b:R;pr:(x:R)``a<x<b``->(derivable_pt f x)) ((x:R)``a<=x<=b``->(continuity_pt f x)) -> ``a<b`` -> (f a)==(f b) -> (EXT c:R | (EXT P: ``a<c<b`` | ``(derive_pt f c (pr c P))==0``)).
-Intros; Assert H2 : (x:R)``a<x<b``->(derivable_pt id x).
-Intros; Apply derivable_pt_id.
-Assert H3 := (TAF_gen f id a b pr H2 H0 H); Assert H4 : (x:R)``a<=x<=b``->(continuity_pt id x).
-Intros; Apply derivable_continuous; Apply derivable_id.
-Elim (H3 H4); Intros; Elim H5; Intros; Exists x; Exists x0; Rewrite H1 in H6; Unfold id in H6; Unfold Rminus in H6; Rewrite Rplus_Ropp_r in H6; Rewrite Rmult_Ol in H6; Apply r_Rmult_mult with ``b-a``; [Rewrite Rmult_Or; Apply H6 | Apply Rminus_eq_contra; Red; Intro; Rewrite H7 in H0; Elim (Rlt_antirefl ? H0)].
-Qed.
-
-(**********)
-Lemma nonneg_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``0<=(derive_pt f x (pr x))``) -> (increasing f).
-Intros.
-Unfold increasing.
-Intros.
-Case (total_order_T x y); Intro.
-Elim s; Intro.
-Apply Rle_anti_compatibility with ``-(f x)``.
-Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
-Assert H1 := (TAF f ? ? pr a).
-Elim H1; Intros.
-Elim H2; Intros.
-Unfold Rminus in H3.
-Rewrite H3.
-Apply Rmult_le_pos.
-Apply H.
-Apply Rle_anti_compatibility with x.
-Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring].
-Rewrite b; Right; Reflexivity.
-Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H0 r)).
-Qed.
- 
-(**********)
-Lemma nonpos_derivative_0 : (f:R->R;pr:(derivable f)) (decreasing f) -> ((x:R) ``(derive_pt f x (pr x))<=0``).
-Intros; Assert H0 :=H; Unfold decreasing in H0; Generalize (derivable_derive f x (pr x)); Intro; Elim H1; Intros l H2.
-Rewrite H2; Case (total_order l R0); Intro.
-Left; Assumption.
-Elim H3; Intro.
-Right; Assumption.
-Generalize (derive_pt_eq_1 f x l (pr x) H2); Intros; Cut ``0< (l/2)``.
-Intro; Elim (H5 ``(l/2)`` H6); Intros delta H7; Cut ``delta/2<>0``/\``0<delta/2``/\``(Rabsolu delta/2)<delta``.
-Intro; Decompose [and] H8; Intros; Generalize (H7 ``delta/2`` H9 H12); Cut ``((f (x+delta/2))-(f x))/(delta/2)<=0``.
-Intro; Cut ``0< -(((f (x+delta/2))-(f x))/(delta/2)-l)``.
-Intro; Unfold Rabsolu; Case (case_Rabsolu ``((f (x+delta/2))-(f x))/(delta/2)-l``).
-Intros; Generalize (Rlt_compatibility_r ``-l`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``(l/2)`` H14); Unfold Rminus.
-Replace ``(l/2)+ -l`` with ``-(l/2)``.
-Replace `` -(((f (x+delta/2))+ -(f x))/(delta/2)+ -l)+ -l`` with ``-(((f (x+delta/2))+ -(f x))/(delta/2))``.
-Intro.
-Generalize (Rlt_Ropp ``-(((f (x+delta/2))+ -(f x))/(delta/2))`` ``-(l/2)`` H15). 
-Repeat Rewrite Ropp_Ropp.
-Intro.
-Generalize (Rlt_trans ``0`` ``l/2`` ``((f (x+delta/2))-(f x))/(delta/2)`` H6 H16); Intro.
-Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``0`` H17 H10)).
-Ring.
-Pattern 3 l; Rewrite double_var.
-Ring.
-Intros.
-Generalize (Rge_Ropp ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` r).
-Rewrite Ropp_O.
-Intro.
-Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``0`` H13 H15)).
-Replace ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` with ``(((f (x))-(f (x+delta/2)))/(delta/2)) +l``.
-Unfold Rminus.
-Apply ge0_plus_gt0_is_gt0.
-Unfold Rdiv; Apply Rmult_le_pos.
-Cut ``x<=(x+(delta*/2))``.
-Intro; Generalize (H0 x ``x+(delta*/2)`` H13); Intro; Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H14); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption.
-Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption.
-Left; Apply Rlt_Rinv; Assumption.
-Assumption.
-Rewrite Ropp_distr2.
-Unfold Rminus.
-Rewrite (Rplus_sym l).
-Unfold Rdiv.
-Rewrite <- Ropp_mul1.
-Rewrite Ropp_distr1.
-Rewrite Ropp_Ropp.
-Rewrite (Rplus_sym (f x)).
-Reflexivity.
-Replace ``((f (x+delta/2))-(f x))/(delta/2)`` with ``-(((f x)-(f (x+delta/2)))/(delta/2))``.
-Rewrite <- Ropp_O.
-Apply Rge_Ropp.
-Apply Rle_sym1.
-Unfold Rdiv; Apply Rmult_le_pos.
-Cut ``x<=(x+(delta*/2))``.
-Intro; Generalize (H0 x ``x+(delta*/2)`` H10); Intro.
-Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H13); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption.
-Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption.
-Left; Apply Rlt_Rinv; Assumption.
-Unfold Rdiv; Rewrite <- Ropp_mul1.
-Rewrite Ropp_distr2.
-Reflexivity.
-Split.
-Unfold Rdiv; Apply prod_neq_R0.
-Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H8; Elim (Rlt_antirefl ``0`` H8).
-Apply Rinv_neq_R0; DiscrR.
-Split.
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Sup0].
-Rewrite Rabsolu_right.
-Unfold Rdiv; Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l; Rewrite double; Pattern 1 (pos delta); Rewrite <- Rplus_Or.
-Apply Rlt_compatibility; Apply (cond_pos delta).
-DiscrR.
-Apply Rle_sym1; Unfold Rdiv; Left; Apply Rmult_lt_pos.
-Apply (cond_pos delta).
-Apply Rlt_Rinv; Sup0.
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply H4 | Apply Rlt_Rinv; Sup0].
-Qed.
-
-(**********)
-Lemma increasing_decreasing_opp : (f:R->R) (increasing f) -> (decreasing (opp_fct f)).
-Unfold increasing decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rge_Ropp; Apply Rle_sym1; Assumption.
-Qed.
-
-(**********)
-Lemma nonpos_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<=0``) -> (decreasing f).
-Intros.
-Cut (h:R)``-(-(f h))==(f h)``.
-Intro.
-Generalize (increasing_decreasing_opp (opp_fct f)).
-Unfold decreasing.
-Unfold opp_fct.
-Intros.
-Rewrite <- (H0 x); Rewrite <- (H0 y).
-Apply H1.
-Cut (x:R)``0<=(derive_pt (opp_fct f) x ((derivable_opp f pr) x))``.
-Intros.
-Replace [x:R]``-(f x)`` with (opp_fct f); [Idtac | Reflexivity].
-Apply (nonneg_derivative_1 (opp_fct f) (derivable_opp f pr) H3).
-Intro.
-Assert H3 := (derive_pt_opp f x0 (pr x0)).
-Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``.
-Intro.
-Rewrite <- H4.
-Rewrite H3.
-Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H x0).
-Apply pr_nu.
-Assumption.
-Intro; Ring.
-Qed.
- 
-(**********)
-Lemma positive_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``0<(derive_pt f x (pr x))``)->(strict_increasing f).
-Intros.
-Unfold strict_increasing.
-Intros.
-Apply Rlt_anti_compatibility with ``-(f x)``.
-Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
-Assert H1 := (TAF f ? ? pr H0).
-Elim H1; Intros.
-Elim H2; Intros.
-Unfold Rminus in H3.
-Rewrite H3.
-Apply Rmult_lt_pos.
-Apply H.
-Apply Rlt_anti_compatibility with x.
-Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring].
-Qed.
-
-(**********)
-Lemma strictincreasing_strictdecreasing_opp : (f:R->R) (strict_increasing f) ->
-(strict_decreasing (opp_fct f)).
-Unfold strict_increasing strict_decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rlt_Ropp; Assumption.
-Qed.
- 
-(**********)
-Lemma negative_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<0``)->(strict_decreasing f).
-Intros.
-Cut (h:R)``- (-(f h))==(f h)``.
-Intros.
-Generalize (strictincreasing_strictdecreasing_opp (opp_fct f)).
-Unfold strict_decreasing opp_fct.
-Intros.
-Rewrite <- (H0 x).
-Rewrite <- (H0 y).
-Apply H1; [Idtac | Assumption].
-Cut (x:R)``0<(derive_pt (opp_fct f) x (derivable_opp f pr x))``.
-Intros; EApply positive_derivative; Apply H3.
-Intro.
-Assert H3 := (derive_pt_opp f x0 (pr x0)).
-Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``.
-Intro.
-Rewrite <- H4; Rewrite H3.
-Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H x0).
-Apply pr_nu.
-Intro; Ring.
-Qed.
- 
-(**********)
-Lemma null_derivative_0 : (f:R->R;pr:(derivable f)) (constant f)->((x:R) ``(derive_pt f x (pr x))==0``). 
-Intros.
-Unfold constant in H.
-Apply derive_pt_eq_0.
-Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Simpl; Intros.
-Rewrite (H x ``x+h``); Unfold Rminus; Unfold Rdiv; Rewrite Rplus_Ropp_r; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
-Qed.
-
-(**********)
-Lemma increasing_decreasing : (f:R->R) (increasing f) -> (decreasing f) -> (constant f).
-Unfold increasing decreasing constant; Intros; Case (total_order x y); Intro.
-Generalize (Rlt_le x y H1); Intro; Apply (Rle_antisym (f x) (f y) (H x y H2) (H0 x y H2)).
-Elim H1; Intro.
-Rewrite H2; Reflexivity.
-Generalize (Rlt_le y x H2); Intro; Symmetry; Apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)).
-Qed.
-
-(**********)
-Lemma null_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))==0``)->(constant f).
-Intros.
-Cut (x:R)``(derive_pt f x (pr x)) <= 0``.
-Cut (x:R)``0 <= (derive_pt f x (pr x))``.
-Intros.
-Assert H2 := (nonneg_derivative_1 f pr H0).
-Assert H3 := (nonpos_derivative_1 f  pr H1).
-Apply increasing_decreasing; Assumption.
-Intro; Right; Symmetry; Apply (H x).
-Intro; Right; Apply (H x).
-Qed.
-
-(**********)
-Lemma derive_increasing_interv_ax : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> (((t:R) ``a<t<b`` -> ``0<(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``)) /\ (((t:R) ``a<t<b`` -> ``0<=(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``)).
-Intros.
-Split; Intros.
-Apply Rlt_anti_compatibility with ``-(f x)``.
-Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
-Assert H4 := (TAF f ? ? pr H3).
-Elim H4; Intros.
-Elim H5; Intros.
-Unfold Rminus in H6.
-Rewrite H6.
-Apply Rmult_lt_pos.
-Apply H0.
-Elim H7; Intros.
-Split.
-Elim H1; Intros.
-Apply Rle_lt_trans with x; Assumption.
-Elim H2; Intros.
-Apply Rlt_le_trans with y; Assumption.
-Apply Rlt_anti_compatibility with x.
-Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring].
-Apply Rle_anti_compatibility with ``-(f x)``.
-Rewrite Rplus_Ropp_l; Rewrite Rplus_sym.
-Assert H4 := (TAF f ? ? pr H3).
-Elim H4; Intros.
-Elim H5; Intros.
-Unfold Rminus in H6.
-Rewrite H6.
-Apply Rmult_le_pos.
-Apply H0.
-Elim H7; Intros.
-Split.
-Elim H1; Intros.
-Apply Rle_lt_trans with x; Assumption.
-Elim H2; Intros.
-Apply Rlt_le_trans with y; Assumption.
-Apply Rle_anti_compatibility with x.
-Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Left; Assumption | Ring].
-Qed.
-
-(**********)
-Lemma derive_increasing_interv : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``).
-Intros.
-Generalize (derive_increasing_interv_ax a b f pr H); Intro.
-Elim H4; Intros H5 _; Apply (H5 H0 x y H1 H2 H3).
-Qed.
-
-(**********)
-Lemma derive_increasing_interv_var : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<=(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``).
-Intros; Generalize (derive_increasing_interv_ax a b f pr H); Intro; Elim H4; Intros _ H5; Apply (H5 H0 x y H1 H2 H3).
-Qed.
-
-(**********)
-(**********)
-Theorem IAF : (f:R->R;a,b,k:R;pr:(derivable f)) ``a<=b`` -> ((c:R) ``a<=c<=b`` -> ``(derive_pt f c (pr c))<=k``) -> ``(f b)-(f a)<=k*(b-a)``.
-Intros.
-Case (total_order_T a b); Intro.
-Elim s; Intro.
-Assert H1 := (TAF f ? ? pr a0).
-Elim H1; Intros.
-Elim H2; Intros.
-Rewrite H3.
-Do 2 Rewrite <- (Rmult_sym ``(b-a)``).
-Apply Rle_monotony.
-Apply Rle_anti_compatibility with ``a``; Rewrite Rplus_Or.
-Replace ``a+(b-a)`` with b; [Assumption | Ring].
-Apply H0.
-Elim H4; Intros.
-Split; Left; Assumption.
-Rewrite b0.
-Unfold Rminus; Do 2 Rewrite Rplus_Ropp_r.
-Rewrite Rmult_Or; Right; Reflexivity.
-Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)).
-Qed.
-
-Lemma IAF_var : (f,g:R->R;a,b:R;pr1:(derivable f);pr2:(derivable g)) ``a<=b`` -> ((c:R) ``a<=c<=b`` -> ``(derive_pt g c (pr2 c))<=(derive_pt f c (pr1 c))``) -> ``(g b)-(g a)<=(f b)-(f a)``.
-Intros.
-Cut (derivable (minus_fct g f)).
-Intro.
-Cut (c:R)``a<=c<=b``->``(derive_pt (minus_fct g f) c (X c))<=0``.
-Intro. 
-Assert H2 := (IAF (minus_fct g f) a b R0 X H H1).
-Rewrite Rmult_Ol in H2; Unfold minus_fct in H2.
-Apply Rle_anti_compatibility with ``-(f b)+(f a)``.
-Replace ``-(f b)+(f a)+((f b)-(f a))`` with R0; [Idtac | Ring].
-Replace ``-(f b)+(f a)+((g b)-(g a))`` with ``(g b)-(f b)-((g a)-(f a))``; [Apply H2 | Ring].
-Intros.
-Cut (derive_pt (minus_fct g f) c (X c))==(derive_pt (minus_fct g f) c (derivable_pt_minus ? ? ? (pr2 c) (pr1 c))).
-Intro.
-Rewrite H2.
-Rewrite derive_pt_minus.
-Apply Rle_anti_compatibility with (derive_pt f c (pr1 c)).
-Rewrite Rplus_Or.
-Replace ``(derive_pt f c (pr1 c))+((derive_pt g c (pr2 c))-(derive_pt f c (pr1 c)))`` with ``(derive_pt g c (pr2 c))``; [Idtac | Ring].
-Apply H0; Assumption.
-Apply pr_nu.
-Apply derivable_minus; Assumption.
-Qed.
-
-(* If f has a null derivative in ]a,b[ and is continue in [a,b], *)
-(* then f is constant on [a,b] *)
-Lemma null_derivative_loc : (f:R->R;a,b:R;pr:(x:R)``a<x<b``->(derivable_pt f x)) ((x:R)``a<=x<=b``->(continuity_pt f x)) -> ((x:R;P:``a<x<b``)(derive_pt f x (pr x P))==R0) -> (constant_D_eq f [x:R]``a<=x<=b`` (f a)).
-Intros; Unfold constant_D_eq; Intros; Case (total_order_T a b); Intro.
-Elim s; Intro.
-Assert H2 : (y:R)``a<y<x``->(derivable_pt id y).
-Intros; Apply derivable_pt_id.
-Assert H3 : (y:R)``a<=y<=x``->(continuity_pt id y).
-Intros; Apply derivable_continuous; Apply derivable_id.
-Assert H4 : (y:R)``a<y<x``->(derivable_pt f y).
-Intros; Apply pr; Elim H4; Intros; Split.
-Assumption.
-Elim H1; Intros; Apply Rlt_le_trans with x; Assumption.
-Assert H5 : (y:R)``a<=y<=x``->(continuity_pt f y).
-Intros; Apply H; Elim H5; Intros; Split.
-Assumption.
-Elim H1; Intros; Apply Rle_trans with x; Assumption.
-Elim H1; Clear H1; Intros; Elim H1; Clear H1; Intro.
-Assert H7 := (TAF_gen f id a x H4 H2 H1 H5 H3).
-Elim H7; Intros; Elim H8; Intros; Assert H10 : ``a<x0<b``.
-Elim x1; Intros; Split.
-Assumption.
-Apply Rlt_le_trans with x; Assumption.
-Assert H11 : ``(derive_pt f x0 (H4 x0 x1))==0``.
-Replace (derive_pt f x0 (H4 x0 x1)) with (derive_pt f x0 (pr x0 H10)); [Apply H0 | Apply pr_nu].
-Assert H12 : ``(derive_pt id x0 (H2 x0 x1))==1``.
-Apply derive_pt_eq_0; Apply derivable_pt_lim_id.
-Rewrite H11 in H9; Rewrite H12 in H9; Rewrite Rmult_Or in H9; Rewrite Rmult_1r in H9; Apply Rminus_eq; Symmetry; Assumption.
-Rewrite H1; Reflexivity.
-Assert H2 : x==a.
-Rewrite <- b0 in H1; Elim H1; Intros; Apply Rle_antisym; Assumption.
-Rewrite H2; Reflexivity.
-Elim H1; Intros; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? (Rle_trans ? ? ? H2 H3) r)).
-Qed.
-
-(* La primitive est unique a une constante pres *)
-Lemma antiderivative_Ucte : (f,g1,g2:R->R;a,b:R) (antiderivative f g1 a b) -> (antiderivative f g2 a b) -> (EXT c:R | (x:R)``a<=x<=b``->``(g1 x)==(g2 x)+c``).
-Unfold antiderivative; Intros; Elim H; Clear H; Intros; Elim H0; Clear H0; Intros H0 _; Exists ``(g1 a)-(g2 a)``; Intros; Assert H3 : (x:R)``a<=x<=b``->(derivable_pt g1 x).
-Intros; Unfold derivable_pt; Apply Specif.existT with (f x0); Elim (H x0 H3); Intros; EApply derive_pt_eq_1; Symmetry; Apply H4.
-Assert H4 : (x:R)``a<=x<=b``->(derivable_pt g2 x).
-Intros; Unfold derivable_pt; Apply Specif.existT with (f x0); Elim (H0 x0 H4); Intros; EApply derive_pt_eq_1; Symmetry; Apply H5.
-Assert H5 : (x:R)``a<x<b``->(derivable_pt (minus_fct g1 g2) x).
-Intros; Elim H5; Intros; Apply derivable_pt_minus; [Apply H3; Split; Left; Assumption | Apply H4; Split; Left; Assumption].
-Assert H6 : (x:R)``a<=x<=b``->(continuity_pt (minus_fct g1 g2) x).
-Intros; Apply derivable_continuous_pt; Apply derivable_pt_minus; [Apply H3 | Apply H4]; Assumption.
-Assert H7 : (x:R;P:``a<x<b``)(derive_pt (minus_fct g1 g2) x (H5 x P))==``0``.
-Intros; Elim P; Intros; Apply derive_pt_eq_0; Replace R0 with ``(f x0)-(f x0)``; [Idtac | Ring].
-Assert H9 : ``a<=x0<=b``.
-Split; Left; Assumption.
-Apply derivable_pt_lim_minus; [Elim (H ? H9) | Elim (H0 ? H9)]; Intros; EApply derive_pt_eq_1; Symmetry; Apply H10.
-Assert H8 := (null_derivative_loc (minus_fct g1 g2) a b H5 H6 H7); Unfold constant_D_eq in H8; Assert H9 := (H8 ? H2); Unfold minus_fct in H9; Rewrite <- H9; Ring.
-Qed.
-- 
cgit v1.2.3