Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1350 insertions, 917 deletions

diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index b8c5c2f4c..f60c609a0 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -8,177 +8,222 @@
 
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
+Require Import Rbase.
+Require Import Rfunctions.
 Require Export Rlimit.
-Require Export Rderiv.
-V7only [Import R_scope.]. Open Local Scope R_scope.
-Implicit Variable Type f:R->R.
+Require Export Rderiv. Open Local Scope R_scope.
+Implicit Type f : R -> R.
 
 (****************************************************)
 (**           Basic operations on functions         *)
 (****************************************************)
-Definition plus_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)+(f2 x)``.
-Definition opp_fct [f:R->R] : R->R := [x:R] ``-(f x)``.
-Definition mult_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)*(f2 x)``.
-Definition mult_real_fct [a:R;f:R->R] : R->R := [x:R] ``a*(f x)``.
-Definition minus_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)-(f2 x)``.
-Definition div_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)/(f2 x)``.
-Definition div_real_fct [a:R;f:R->R] : R->R := [x:R] ``a/(f x)``.
-Definition comp [f1,f2:R->R] : R->R := [x:R] ``(f1 (f2 x))``.
-Definition inv_fct [f:R->R] : R->R := [x:R]``/(f x)``.
-
-V8Infix "+" plus_fct : Rfun_scope.
-V8Notation "- x" := (opp_fct x) : Rfun_scope.
-V8Infix "*" mult_fct : Rfun_scope.
-V8Infix "-" minus_fct : Rfun_scope.
-V8Infix "/" div_fct : Rfun_scope.
-Notation Local "f1 'o' f2" := (comp f1 f2) (at level 2, right associativity)
-  : Rfun_scope 
-  V8only (at level 20, right associativity).
-V8Notation "/ x" := (inv_fct x) : Rfun_scope.
-
-Delimits Scope Rfun_scope with F.
-
-Definition fct_cte [a:R] : R->R := [x:R]a.
-Definition id := [x:R]x.
+Definition plus_fct f1 f2 (x:R) : R := f1 x + f2 x.
+Definition opp_fct f (x:R) : R := - f x.
+Definition mult_fct f1 f2 (x:R) : R := f1 x * f2 x.
+Definition mult_real_fct (a:R) f (x:R) : R := a * f x.
+Definition minus_fct f1 f2 (x:R) : R := f1 x - f2 x.
+Definition div_fct f1 f2 (x:R) : R := f1 x / f2 x.
+Definition div_real_fct (a:R) f (x:R) : R := a / f x.
+Definition comp f1 f2 (x:R) : R := f1 (f2 x).
+Definition inv_fct f (x:R) : R := / f x.
+
+Infix "+" := plus_fct : Rfun_scope.
+Notation "- x" := (opp_fct x) : Rfun_scope.
+Infix "*" := mult_fct : Rfun_scope.
+Infix "-" := minus_fct : Rfun_scope.
+Infix "/" := div_fct : Rfun_scope.
+Notation Local "f1 'o' f2" := (comp f1 f2)
+  (at level 20, right associativity) : Rfun_scope.
+Notation "/ x" := (inv_fct x) : Rfun_scope.
+
+Delimit Scope Rfun_scope with F.
+
+Definition fct_cte (a x:R) : R := a.
+Definition id (x:R) := x.
 
 (****************************************************)
 (**            Variations of functions              *)
 (****************************************************)
-Definition increasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f x)<=(f y)``.
-Definition decreasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f y)<=(f x)``.
-Definition strict_increasing [f:R->R] : Prop := (x,y:R) ``x<y``->``(f x)<(f y)``.
-Definition strict_decreasing [f:R->R] : Prop := (x,y:R) ``x<y``->``(f y)<(f x)``.
-Definition constant [f:R->R] : Prop := (x,y:R) ``(f x)==(f y)``.
+Definition increasing f : Prop := forall x y:R, x <= y -> f x <= f y.
+Definition decreasing f : Prop := forall x y:R, x <= y -> f y <= f x.
+Definition strict_increasing f : Prop := forall x y:R, x < y -> f x < f y.
+Definition strict_decreasing f : Prop := forall x y:R, x < y -> f y < f x.
+Definition constant f : Prop := forall x y:R, f x = f y.
   
 (**********) 
-Definition no_cond : R->Prop := [x:R] True.
+Definition no_cond (x:R) : Prop := True.
 
 (**********)
-Definition constant_D_eq [f:R->R;D:R->Prop;c:R] : Prop := (x:R) (D x) -> (f x)==c.
+Definition constant_D_eq f (D:R -> Prop) (c:R) : Prop :=
+  forall x:R, D x -> f x = c.
 
 (***************************************************)
 (**      Definition of continuity as a limit       *)
 (***************************************************)
 
 (**********)
-Definition continuity_pt [f:R->R; x0:R] : Prop := (continue_in f no_cond x0).
-Definition continuity [f:R->R] : Prop := (x:R) (continuity_pt f x).
+Definition continuity_pt f (x0:R) : Prop := continue_in f no_cond x0.
+Definition continuity f : Prop := forall x:R, continuity_pt f x.
 
 Arguments Scope continuity_pt [Rfun_scope R_scope].
 Arguments Scope continuity [Rfun_scope].
 
 (**********)
-Lemma continuity_pt_plus : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (plus_fct f1 f2) x0).
-Unfold continuity_pt plus_fct; Unfold continue_in; Intros; Apply limit_plus; Assumption.
+Lemma continuity_pt_plus :
+ forall f1 f2 (x0:R),
+   continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 + f2) x0.
+unfold continuity_pt, plus_fct in |- *; unfold continue_in in |- *; intros;
+ apply limit_plus; assumption.
 Qed.
 
-Lemma continuity_pt_opp : (f:R->R; x0:R) (continuity_pt f x0) -> (continuity_pt (opp_fct f) x0).
-Unfold continuity_pt opp_fct; Unfold continue_in; Intros; Apply limit_Ropp; Assumption.
+Lemma continuity_pt_opp :
+ forall f (x0:R), continuity_pt f x0 -> continuity_pt (- f) x0.
+unfold continuity_pt, opp_fct in |- *; unfold continue_in in |- *; intros;
+ apply limit_Ropp; assumption.
 Qed.
  
-Lemma continuity_pt_minus : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (minus_fct f1 f2) x0).
-Unfold continuity_pt minus_fct; Unfold continue_in; Intros; Apply limit_minus; Assumption.
-Qed.
-
-Lemma continuity_pt_mult : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (mult_fct f1 f2) x0).
-Unfold continuity_pt mult_fct; Unfold continue_in; Intros; Apply limit_mul; Assumption.
-Qed.
-
-Lemma continuity_pt_const : (f:R->R; x0:R) (constant f) -> (continuity_pt f x0).
-Unfold constant continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split; [Apply Rlt_R0_R1 | Intros; Generalize (H x x0); Intro; Rewrite H2; Simpl; Rewrite R_dist_eq; Assumption].
-Qed.
-
-Lemma continuity_pt_scal : (f:R->R;a:R; x0:R) (continuity_pt f x0) -> (continuity_pt (mult_real_fct a f) x0).
-Unfold continuity_pt mult_real_fct; Unfold continue_in; Intros; Apply (limit_mul ([x:R] a) f (D_x no_cond x0) a (f x0) x0).
-Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split.
-Apply Rlt_R0_R1.
-Intros; Rewrite R_dist_eq; Assumption.
-Assumption.
-Qed.
-
-Lemma continuity_pt_inv : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> (continuity_pt (inv_fct f) x0).
-Intros.
-Replace (inv_fct f) with [x:R]``/(f x)``.
-Unfold continuity_pt; Unfold continue_in; Intros; Apply limit_inv; Assumption.
-Unfold inv_fct; Reflexivity.
+Lemma continuity_pt_minus :
+ forall f1 f2 (x0:R),
+   continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 - f2) x0.
+unfold continuity_pt, minus_fct in |- *; unfold continue_in in |- *; intros;
+ apply limit_minus; assumption.
+Qed.
+
+Lemma continuity_pt_mult :
+ forall f1 f2 (x0:R),
+   continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 * f2) x0.
+unfold continuity_pt, mult_fct in |- *; unfold continue_in in |- *; intros;
+ apply limit_mul; assumption.
+Qed.
+
+Lemma continuity_pt_const : forall f (x0:R), constant f -> continuity_pt f x0.
+unfold constant, continuity_pt in |- *; unfold continue_in in |- *;
+ unfold limit1_in in |- *; unfold limit_in in |- *; 
+ intros; exists 1; split;
+ [ apply Rlt_0_1
+ | intros; generalize (H x x0); intro; rewrite H2; simpl in |- *;
+    rewrite R_dist_eq; assumption ].
+Qed.
+
+Lemma continuity_pt_scal :
+ forall f (a x0:R),
+   continuity_pt f x0 -> continuity_pt (mult_real_fct a f) x0.
+unfold continuity_pt, mult_real_fct in |- *; unfold continue_in in |- *;
+ intros; apply (limit_mul (fun x:R => a) f (D_x no_cond x0) a (f x0) x0).
+unfold limit1_in in |- *; unfold limit_in in |- *; intros; exists 1; split.
+apply Rlt_0_1.
+intros; rewrite R_dist_eq; assumption.
+assumption.
+Qed.
+
+Lemma continuity_pt_inv :
+ forall f (x0:R), continuity_pt f x0 -> f x0 <> 0 -> continuity_pt (/ f) x0.
+intros.
+replace (/ f)%F with (fun x:R => / f x).
+unfold continuity_pt in |- *; unfold continue_in in |- *; intros;
+ apply limit_inv; assumption.
+unfold inv_fct in |- *; reflexivity.
 Qed.
  
-Lemma div_eq_inv : (f1,f2:R->R) (div_fct f1 f2)==(mult_fct f1 (inv_fct f2)).
-Intros; Reflexivity.
+Lemma div_eq_inv : forall f1 f2, (f1 / f2)%F = (f1 * / f2)%F.
+intros; reflexivity.
 Qed.
  
-Lemma continuity_pt_div : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> ~``(f2 x0)==0`` -> (continuity_pt (div_fct f1 f2) x0).
-Intros; Rewrite -> (div_eq_inv f1 f2); Apply continuity_pt_mult; [Assumption | Apply continuity_pt_inv; Assumption].
-Qed.
-
-Lemma continuity_pt_comp : (f1,f2:R->R;x:R) (continuity_pt f1 x) -> (continuity_pt f2 (f1 x)) -> (continuity_pt (comp f2 f1) x).
-Unfold continuity_pt; Unfold continue_in; Intros; Unfold comp.
-Cut (limit1_in [x0:R](f2 (f1 x0)) (Dgf (D_x no_cond x) (D_x no_cond (f1 x)) f1)
-(f2 (f1 x)) x) -> (limit1_in [x0:R](f2 (f1 x0)) (D_x no_cond x) (f2 (f1 x)) x).
-Intro; Apply H1.
-EApply limit_comp.
-Apply H.
-Apply H0.
-Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros.
-Assert H3 := (H1 eps H2).
-Elim H3; Intros.
-Exists x0.
-Split.
-Elim H4; Intros; Assumption.
-Intros; Case (Req_EM (f1 x) (f1 x1)); Intro.
-Rewrite H6; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
-Elim H4; Intros; Apply H8.
-Split.
-Unfold Dgf D_x no_cond.
-Split.
-Split.
-Trivial.
-Elim H5; Unfold D_x no_cond; Intros.
-Elim H9; Intros; Assumption.
-Split.
-Trivial.
-Assumption.
-Elim H5; Intros; Assumption.
+Lemma continuity_pt_div :
+ forall f1 f2 (x0:R),
+   continuity_pt f1 x0 ->
+   continuity_pt f2 x0 -> f2 x0 <> 0 -> continuity_pt (f1 / f2) x0.
+intros; rewrite (div_eq_inv f1 f2); apply continuity_pt_mult;
+ [ assumption | apply continuity_pt_inv; assumption ].
+Qed.
+
+Lemma continuity_pt_comp :
+ forall f1 f2 (x:R),
+   continuity_pt f1 x -> continuity_pt f2 (f1 x) -> continuity_pt (f2 o f1) x.
+unfold continuity_pt in |- *; unfold continue_in in |- *; intros;
+ unfold comp in |- *.
+cut
+ (limit1_in (fun x0:R => f2 (f1 x0))
+    (Dgf (D_x no_cond x) (D_x no_cond (f1 x)) f1) (
+    f2 (f1 x)) x ->
+  limit1_in (fun x0:R => f2 (f1 x0)) (D_x no_cond x) (f2 (f1 x)) x).
+intro; apply H1.
+eapply limit_comp.
+apply H.
+apply H0.
+unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
+ simpl in |- *; unfold R_dist in |- *; intros.
+assert (H3 := H1 eps H2).
+elim H3; intros.
+exists x0.
+split.
+elim H4; intros; assumption.
+intros; case (Req_dec (f1 x) (f1 x1)); intro.
+rewrite H6; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
+ assumption.
+elim H4; intros; apply H8.
+split.
+unfold Dgf, D_x, no_cond in |- *.
+split.
+split.
+trivial.
+elim H5; unfold D_x, no_cond in |- *; intros.
+elim H9; intros; assumption.
+split.
+trivial.
+assumption.
+elim H5; intros; assumption.
 Qed.
 
 (**********) 
-Lemma continuity_plus : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (plus_fct f1 f2)).
-Unfold continuity; Intros; Apply (continuity_pt_plus f1 f2 x (H x) (H0 x)).
+Lemma continuity_plus :
+ forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 + f2).
+unfold continuity in |- *; intros;
+ apply (continuity_pt_plus f1 f2 x (H x) (H0 x)).
 Qed.
 
-Lemma continuity_opp : (f:R->R) (continuity f)->(continuity (opp_fct f)).
-Unfold continuity; Intros; Apply (continuity_pt_opp f x (H x)).
+Lemma continuity_opp : forall f, continuity f -> continuity (- f).
+unfold continuity in |- *; intros; apply (continuity_pt_opp f x (H x)).
 Qed.
 
-Lemma continuity_minus : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (minus_fct f1 f2)).
-Unfold continuity; Intros; Apply (continuity_pt_minus f1 f2 x (H x) (H0 x)).
+Lemma continuity_minus :
+ forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 - f2).
+unfold continuity in |- *; intros;
+ apply (continuity_pt_minus f1 f2 x (H x) (H0 x)).
 Qed.
  
-Lemma continuity_mult : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (mult_fct f1 f2)).
-Unfold continuity; Intros; Apply (continuity_pt_mult f1 f2 x (H x) (H0 x)).
+Lemma continuity_mult :
+ forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 * f2).
+unfold continuity in |- *; intros;
+ apply (continuity_pt_mult f1 f2 x (H x) (H0 x)).
 Qed.
 
-Lemma continuity_const : (f:R->R) (constant f) -> (continuity f).
-Unfold continuity; Intros; Apply (continuity_pt_const f x H).
+Lemma continuity_const : forall f, constant f -> continuity f.
+unfold continuity in |- *; intros; apply (continuity_pt_const f x H).
 Qed.
 
-Lemma continuity_scal : (f:R->R;a:R) (continuity f) -> (continuity (mult_real_fct a f)).
-Unfold continuity; Intros; Apply (continuity_pt_scal f a x (H x)).
+Lemma continuity_scal :
+ forall f (a:R), continuity f -> continuity (mult_real_fct a f).
+unfold continuity in |- *; intros; apply (continuity_pt_scal f a x (H x)).
 Qed.
   
-Lemma continuity_inv : (f:R->R) (continuity f)->((x:R) ~``(f x)==0``)->(continuity (inv_fct f)).
-Unfold continuity; Intros; Apply (continuity_pt_inv f x (H x) (H0 x)).
+Lemma continuity_inv :
+ forall f, continuity f -> (forall x:R, f x <> 0) -> continuity (/ f).
+unfold continuity in |- *; intros; apply (continuity_pt_inv f x (H x) (H0 x)).
 Qed.
 
-Lemma continuity_div : (f1,f2:R->R) (continuity f1)->(continuity f2)->((x:R) ~``(f2 x)==0``)->(continuity (div_fct f1 f2)).
-Unfold continuity; Intros; Apply (continuity_pt_div f1 f2 x (H x) (H0 x) (H1 x)).
+Lemma continuity_div :
+ forall f1 f2,
+   continuity f1 ->
+   continuity f2 -> (forall x:R, f2 x <> 0) -> continuity (f1 / f2).
+unfold continuity in |- *; intros;
+ apply (continuity_pt_div f1 f2 x (H x) (H0 x) (H1 x)).
 Qed.
  
-Lemma continuity_comp : (f1,f2:R->R) (continuity f1) -> (continuity f2) -> (continuity (comp f2 f1)).
-Unfold continuity; Intros.
-Apply (continuity_pt_comp f1 f2 x (H x) (H0 (f1 x))).
+Lemma continuity_comp :
+ forall f1 f2, continuity f1 -> continuity f2 -> continuity (f2 o f1).
+unfold continuity in |- *; intros.
+apply (continuity_pt_comp f1 f2 x (H x) (H0 (f1 x))).
 Qed.
 
 
@@ -186,15 +231,20 @@ Qed.
 (**  Derivative's definition using Landau's kernel   *)
 (*****************************************************)
 
-Definition derivable_pt_lim [f:R->R;x,l:R] : Prop := ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``))).
+Definition derivable_pt_lim f (x l:R) : Prop :=
+  forall eps:R,
+    0 < eps ->
+     exists delta : posreal
+    | (forall h:R,
+         h <> 0 -> Rabs h < delta -> Rabs ((f (x + h) - f x) / h - l) < eps).
 
-Definition derivable_pt_abs [f:R->R;x:R] : R -> Prop := [l:R](derivable_pt_lim f x l).
+Definition derivable_pt_abs f (x l:R) : Prop := derivable_pt_lim f x l.
 
-Definition derivable_pt [f:R->R;x:R] := (SigT R (derivable_pt_abs f x)).
-Definition derivable [f:R->R] := (x:R)(derivable_pt f x).
+Definition derivable_pt f (x:R) := sigT (derivable_pt_abs f x).
+Definition derivable f := forall x:R, derivable_pt f x.
 
-Definition derive_pt [f:R->R;x:R;pr:(derivable_pt f x)] := (projT1 ? ? pr).
-Definition derive [f:R->R;pr:(derivable f)] := [x:R](derive_pt f x (pr x)).
+Definition derive_pt f (x:R) (pr:derivable_pt f x) := projT1 pr.
+Definition derive f (pr:derivable f) (x:R) := derive_pt f x (pr x).
 
 Arguments Scope derivable_pt_lim [Rfun_scope R_scope].
 Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope].
@@ -203,125 +253,191 @@ Arguments Scope derivable [Rfun_scope].
 Arguments Scope derive_pt [Rfun_scope R_scope _].
 Arguments Scope derive [Rfun_scope _].
 
-Definition antiderivative [f,g:R->R;a,b:R] : Prop := ((x:R)``a<=x<=b``->(EXT pr : (derivable_pt g x) | (f x)==(derive_pt g x pr)))/\``a<=b``.
+Definition antiderivative f (g:R -> R) (a b:R) : Prop :=
+  (forall x:R,
+     a <= x <= b ->  exists pr : derivable_pt g x | f x = derive_pt g x pr) /\
+  a <= b.
 (************************************)
 (** Class of differential functions *)
 (************************************)
-Record Differential : Type := mkDifferential {
-d1 :> R->R;
-cond_diff : (derivable d1) }.
+Record Differential : Type := mkDifferential
+  {d1 :> R -> R; cond_diff : derivable d1}.
  
-Record Differential_D2 : Type := mkDifferential_D2 {
-d2 :> R->R;
-cond_D1 : (derivable d2);
-cond_D2 : (derivable (derive d2 cond_D1)) }.
+Record Differential_D2 : Type := mkDifferential_D2
+  {d2 :> R -> R;
+   cond_D1 : derivable d2;
+   cond_D2 : derivable (derive d2 cond_D1)}.
 
 (**********)
-Lemma unicite_step1 : (f:R->R;x,l1,l2:R) (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l1 R0) -> (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l2 R0) -> l1 == l2.
-Intros; Apply (single_limit [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l1 l2 R0); Try Assumption.
-Unfold adhDa; Intros; Exists ``alp/2``.
-Split.
-Unfold Rdiv; Apply prod_neq_R0.
-Red; Intro; Rewrite H2 in H1; Elim (Rlt_antirefl ? H1).
-Apply Rinv_neq_R0; DiscrR.
-Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Unfold Rdiv; Rewrite Rabsolu_mult.
-Replace ``(Rabsolu (/2))`` with ``/2``.
-Replace (Rabsolu alp) with alp.
-Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1r; Rewrite double; Pattern 1 alp; Replace alp with ``alp+0``; [Idtac | Ring]; Apply Rlt_compatibility; Assumption.
-Symmetry; Apply Rabsolu_right; Left; Assumption.
-Symmetry; Apply Rabsolu_right; Left; Change ``0</2``; Apply Rlt_Rinv; Sup0. 
-Qed.
-
-Lemma unicite_step2 : (f:R->R;x,l:R) (derivable_pt_lim f x l) -> (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l R0).
-Unfold derivable_pt_lim; Intros; Unfold limit1_in; Unfold limit_in; Intros.
-Assert H1 := (H eps H0).
-Elim H1 ; Intros.
-Exists (pos x0).
-Split.
-Apply (cond_pos x0).
-Simpl; Unfold R_dist; Intros.
-Elim H3; Intros.
-Apply H2; [Assumption |Unfold Rminus in H5; Rewrite Ropp_O in H5; Rewrite Rplus_Or in H5; Assumption].
-Qed.
-
-Lemma unicite_step3 : (f:R->R;x,l:R) (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l R0) -> (derivable_pt_lim f x l).
-Unfold limit1_in derivable_pt_lim; Unfold limit_in; Unfold dist; Simpl; Intros.
-Elim (H eps H0).
-Intros; Elim H1; Intros.
-Exists (mkposreal x0 H2).
-Simpl; Intros; Unfold R_dist in H3; Apply (H3 h).
-Split; [Assumption | Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Assumption].
-Qed.
-
-Lemma unicite_limite : (f:R->R;x,l1,l2:R) (derivable_pt_lim f x l1) -> (derivable_pt_lim f x l2) -> l1==l2.
-Intros.
-Assert H1 := (unicite_step2 ? ? ? H).
-Assert H2 := (unicite_step2 ? ? ? H0).
-Assert H3 := (unicite_step1 ? ? ? ? H1 H2).
-Assumption.
-Qed.
-
-Lemma derive_pt_eq : (f:R->R;x,l:R;pr:(derivable_pt f x)) (derive_pt f x pr)==l <-> (derivable_pt_lim f x l).
-Intros; Split.
-Intro; Assert H1 := (projT2 ? ? pr); Unfold derive_pt in H; Rewrite H in H1; Assumption.
-Intro; Assert H1 := (projT2 ? ? pr); Unfold derivable_pt_abs in H1.
-Assert H2 := (unicite_limite ? ? ? ? H H1).
-Unfold derive_pt; Unfold derivable_pt_abs.
-Symmetry; Assumption.
+Lemma uniqueness_step1 :
+ forall f (x l1 l2:R),
+   limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l1 0 ->
+   limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l2 0 ->
+   l1 = l2.
+intros;
+ apply
+  (single_limit (fun h:R => (f (x + h) - f x) / h) (
+     fun h:R => h <> 0) l1 l2 0); try assumption.
+unfold adhDa in |- *; intros; exists (alp / 2).
+split.
+unfold Rdiv in |- *; apply prod_neq_R0.
+red in |- *; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1).
+apply Rinv_neq_0_compat; discrR.
+unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0;
+ rewrite Rplus_0_r; unfold Rdiv in |- *; rewrite Rabs_mult.
+replace (Rabs (/ 2)) with (/ 2).
+replace (Rabs alp) with alp.
+apply Rmult_lt_reg_l with 2.
+prove_sup0.
+rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite <- Rinv_l_sym;
+ [ idtac | discrR ]; rewrite Rmult_1_r; rewrite double;
+ pattern alp at 1 in |- *; replace alp with (alp + 0); 
+ [ idtac | ring ]; apply Rplus_lt_compat_l; assumption.
+symmetry  in |- *; apply Rabs_right; left; assumption.
+symmetry  in |- *; apply Rabs_right; left; change (0 < / 2) in |- *;
+ apply Rinv_0_lt_compat; prove_sup0. 
+Qed.
+
+Lemma uniqueness_step2 :
+ forall f (x l:R),
+   derivable_pt_lim f x l ->
+   limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0.
+unfold derivable_pt_lim in |- *; intros; unfold limit1_in in |- *;
+ unfold limit_in in |- *; intros.
+assert (H1 := H eps H0).
+elim H1; intros.
+exists (pos x0).
+split.
+apply (cond_pos x0).
+simpl in |- *; unfold R_dist in |- *; intros.
+elim H3; intros.
+apply H2;
+ [ assumption
+ | unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5;
+    assumption ].
+Qed.
+
+Lemma uniqueness_step3 :
+ forall f (x l:R),
+   limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0 ->
+   derivable_pt_lim f x l.
+unfold limit1_in, derivable_pt_lim in |- *; unfold limit_in in |- *;
+ unfold dist in |- *; simpl in |- *; intros.
+elim (H eps H0).
+intros; elim H1; intros.
+exists (mkposreal x0 H2).
+simpl in |- *; intros; unfold R_dist in H3; apply (H3 h).
+split;
+ [ assumption
+ | unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; assumption ].
+Qed.
+
+Lemma uniqueness_limite :
+ forall f (x l1 l2:R),
+   derivable_pt_lim f x l1 -> derivable_pt_lim f x l2 -> l1 = l2.
+intros.
+assert (H1 := uniqueness_step2 _ _ _ H).
+assert (H2 := uniqueness_step2 _ _ _ H0).
+assert (H3 := uniqueness_step1 _ _ _ _ H1 H2).
+assumption.
+Qed.
+
+Lemma derive_pt_eq :
+ forall f (x l:R) (pr:derivable_pt f x),
+   derive_pt f x pr = l <-> derivable_pt_lim f x l.
+intros; split.
+intro; assert (H1 := projT2 pr); unfold derive_pt in H; rewrite H in H1;
+ assumption.
+intro; assert (H1 := projT2 pr); unfold derivable_pt_abs in H1.
+assert (H2 := uniqueness_limite _ _ _ _ H H1).
+unfold derive_pt in |- *; unfold derivable_pt_abs in |- *.
+symmetry  in |- *; assumption.
 Qed.
 
 (**********)
-Lemma derive_pt_eq_0 : (f:R->R;x,l:R;pr:(derivable_pt f x)) (derivable_pt_lim f x l) -> (derive_pt f x pr)==l.
-Intros; Elim (derive_pt_eq f x l pr); Intros.
-Apply (H1 H).
+Lemma derive_pt_eq_0 :
+ forall f (x l:R) (pr:derivable_pt f x),
+   derivable_pt_lim f x l -> derive_pt f x pr = l.
+intros; elim (derive_pt_eq f x l pr); intros.
+apply (H1 H).
 Qed.
 
 (**********)
-Lemma derive_pt_eq_1 : (f:R->R;x,l:R;pr:(derivable_pt f x)) (derive_pt f x pr)==l -> (derivable_pt_lim f x l).
-Intros; Elim (derive_pt_eq f x l pr); Intros.
-Apply (H0 H).
+Lemma derive_pt_eq_1 :
+ forall f (x l:R) (pr:derivable_pt f x),
+   derive_pt f x pr = l -> derivable_pt_lim f x l.
+intros; elim (derive_pt_eq f x l pr); intros.
+apply (H0 H).
 Qed.
 
 
 (********************************************************************)
 (** Equivalence of this definition with the one using limit concept *)
 (********************************************************************)
-Lemma derive_pt_D_in : (f,df:R->R;x:R;pr:(derivable_pt f x)) (D_in f df no_cond x) <-> (derive_pt f x pr)==(df x).
-Intros; Split.
-Unfold D_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros.
-Apply derive_pt_eq_0. 
-Unfold derivable_pt_lim.
-Intros; Elim (H eps H0); Intros alpha H1; Elim H1; Intros;  Exists (mkposreal alpha H2); Intros; Generalize (H3 ``x+h``); Intro; Cut ``x+h-x==h``; [Intro; Cut ``(D_x no_cond x (x+h))``/\``(Rabsolu (x+h-x)) < alpha``; [Intro; Generalize (H6 H8); Rewrite H7; Intro; Assumption | Split; [Unfold D_x; Split; [Unfold no_cond; Trivial | Apply Rminus_not_eq_right; Rewrite H7; Assumption] | Rewrite H7; Assumption]] | Ring].
-Intro.
-Assert H0 := (derive_pt_eq_1 f x (df x) pr H).
-Unfold D_in; Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros.
-Elim (H0 eps H1); Intros alpha H2; Exists (pos alpha); Split.
-Apply (cond_pos alpha).
-Intros; Elim H3; Intros; Unfold D_x in H4; Elim H4; Intros; Cut ``x0-x<>0``.
-Intro; Generalize (H2 ``x0-x`` H8 H5); Replace ``x+(x0-x)`` with x0.
-Intro; Assumption.
-Ring.
-Auto with real.
-Qed.
-
-Lemma derivable_pt_lim_D_in : (f,df:R->R;x:R) (D_in f df no_cond x) <-> (derivable_pt_lim f x (df x)).
-Intros; Split.
-Unfold D_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros.
-Unfold derivable_pt_lim.
-Intros; Elim (H eps H0); Intros alpha H1; Elim H1; Intros;  Exists (mkposreal alpha H2); Intros; Generalize (H3 ``x+h``); Intro; Cut ``x+h-x==h``; [Intro; Cut ``(D_x no_cond x (x+h))``/\``(Rabsolu (x+h-x)) < alpha``; [Intro; Generalize (H6 H8); Rewrite H7; Intro; Assumption | Split; [Unfold D_x; Split; [Unfold no_cond; Trivial | Apply Rminus_not_eq_right; Rewrite H7; Assumption] | Rewrite H7; Assumption]] | Ring].
-Intro.
-Unfold derivable_pt_lim in H.
-Unfold D_in; Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros.
-Elim (H eps H0); Intros alpha H2; Exists (pos alpha); Split.
-Apply (cond_pos alpha).
-Intros.
-Elim H1; Intros; Unfold D_x in H3; Elim H3; Intros; Cut ``x0-x<>0``.
-Intro; Generalize (H2 ``x0-x`` H7 H4); Replace ``x+(x0-x)`` with x0.
-Intro; Assumption.
-Ring.
-Auto with real.
+Lemma derive_pt_D_in :
+ forall f (df:R -> R) (x:R) (pr:derivable_pt f x),
+   D_in f df no_cond x <-> derive_pt f x pr = df x.
+intros; split.
+unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
+ simpl in |- *; unfold R_dist in |- *; intros.
+apply derive_pt_eq_0. 
+unfold derivable_pt_lim in |- *.
+intros; elim (H eps H0); intros alpha H1; elim H1; intros;
+ exists (mkposreal alpha H2); intros; generalize (H3 (x + h)); 
+ intro; cut (x + h - x = h);
+ [ intro; cut (D_x no_cond x (x + h) /\ Rabs (x + h - x) < alpha);
+    [ intro; generalize (H6 H8); rewrite H7; intro; assumption
+    | split;
+       [ unfold D_x in |- *; split;
+          [ unfold no_cond in |- *; trivial
+          | apply Rminus_not_eq_right; rewrite H7; assumption ]
+       | rewrite H7; assumption ] ]
+ | ring ].
+intro.
+assert (H0 := derive_pt_eq_1 f x (df x) pr H).
+unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
+ unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; 
+ intros.
+elim (H0 eps H1); intros alpha H2; exists (pos alpha); split.
+apply (cond_pos alpha).
+intros; elim H3; intros; unfold D_x in H4; elim H4; intros; cut (x0 - x <> 0).
+intro; generalize (H2 (x0 - x) H8 H5); replace (x + (x0 - x)) with x0.
+intro; assumption.
+ring.
+auto with real.
+Qed.
+
+Lemma derivable_pt_lim_D_in :
+ forall f (df:R -> R) (x:R),
+   D_in f df no_cond x <-> derivable_pt_lim f x (df x).
+intros; split.
+unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
+ simpl in |- *; unfold R_dist in |- *; intros.
+unfold derivable_pt_lim in |- *.
+intros; elim (H eps H0); intros alpha H1; elim H1; intros;
+ exists (mkposreal alpha H2); intros; generalize (H3 (x + h)); 
+ intro; cut (x + h - x = h);
+ [ intro; cut (D_x no_cond x (x + h) /\ Rabs (x + h - x) < alpha);
+    [ intro; generalize (H6 H8); rewrite H7; intro; assumption
+    | split;
+       [ unfold D_x in |- *; split;
+          [ unfold no_cond in |- *; trivial
+          | apply Rminus_not_eq_right; rewrite H7; assumption ]
+       | rewrite H7; assumption ] ]
+ | ring ].
+intro.
+unfold derivable_pt_lim in H.
+unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *;
+ unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; 
+ intros.
+elim (H eps H0); intros alpha H2; exists (pos alpha); split.
+apply (cond_pos alpha).
+intros.
+elim H1; intros; unfold D_x in H3; elim H3; intros; cut (x0 - x <> 0).
+intro; generalize (H2 (x0 - x) H7 H4); replace (x + (x0 - x)) with x0.
+intro; assumption.
+ring.
+auto with real.
 Qed.
 
 
@@ -329,457 +445,555 @@ Qed.
 (**   derivability -> continuity   *)
 (***********************************)
 (**********)
-Lemma derivable_derive : (f:R->R;x:R;pr:(derivable_pt f x)) (EXT l : R | (derive_pt f x pr)==l).
-Intros; Exists (projT1  ? ? pr).
-Unfold derive_pt; Reflexivity.
+Lemma derivable_derive :
+ forall f (x:R) (pr:derivable_pt f x),  exists l : R | derive_pt f x pr = l.
+intros; exists (projT1 pr).
+unfold derive_pt in |- *; reflexivity.
 Qed.
 
-Theorem derivable_continuous_pt : (f:R->R;x:R) (derivable_pt f x) -> (continuity_pt f x).
-Intros.
-Generalize (derivable_derive f x X); Intro.
-Elim H; Intros l H1.
-Cut l==((fct_cte l) x).
-Intro.
-Rewrite H0 in H1.
-Generalize (derive_pt_D_in f (fct_cte l) x); Intro.
-Elim (H2 X); Intros.
-Generalize (H4 H1); Intro.
-Unfold continuity_pt.
-Apply (cont_deriv f (fct_cte l) no_cond x H5).
-Unfold fct_cte; Reflexivity.
+Theorem derivable_continuous_pt :
+ forall f (x:R), derivable_pt f x -> continuity_pt f x.
+intros.
+generalize (derivable_derive f x X); intro.
+elim H; intros l H1.
+cut (l = fct_cte l x).
+intro.
+rewrite H0 in H1.
+generalize (derive_pt_D_in f (fct_cte l) x); intro.
+elim (H2 X); intros.
+generalize (H4 H1); intro.
+unfold continuity_pt in |- *.
+apply (cont_deriv f (fct_cte l) no_cond x H5).
+unfold fct_cte in |- *; reflexivity.
 Qed.
 
-Theorem derivable_continuous : (f:R->R) (derivable f) -> (continuity f).
-Unfold derivable continuity; Intros.
-Apply (derivable_continuous_pt f x (X x)).
+Theorem derivable_continuous : forall f, derivable f -> continuity f.
+unfold derivable, continuity in |- *; intros.
+apply (derivable_continuous_pt f x (X x)).
 Qed.
 
 (****************************************************************)
 (**                      Main rules                             *)
 (****************************************************************)
 
-Lemma derivable_pt_lim_plus : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (plus_fct f1 f2) x ``l1+l2``).
-Intros.
-Apply unicite_step3.
-Assert H1 := (unicite_step2 ? ? ? H).
-Assert H2 := (unicite_step2 ? ? ? H0).
-Unfold  plus_fct.
-Cut (h:R)``((f1 (x+h))+(f2 (x+h))-((f1 x)+(f2 x)))/h``==``((f1 (x+h))-(f1 x))/h+((f2 (x+h))-(f2 x))/h``.
-Intro.
-Generalize(limit_plus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2).
-Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros.
-Elim (H4 eps H5); Intros.
-Exists x0.
-Elim H6; Intros.
-Split.
-Assumption.
-Intros; Rewrite H3; Apply H8; Assumption.
-Intro; Unfold Rdiv; Ring.
-Qed.
-
-Lemma derivable_pt_lim_opp : (f:R->R;x,l:R) (derivable_pt_lim f x l) -> (derivable_pt_lim (opp_fct f) x (Ropp l)).
-Intros.
-Apply unicite_step3.
-Assert H1 := (unicite_step2 ? ? ? H).
-Unfold opp_fct.
-Cut (h:R) ``( -(f (x+h))- -(f x))/h``==(Ropp ``((f (x+h))-(f x))/h``).
-Intro.
-Generalize (limit_Ropp [h:R]``((f (x+h))-(f x))/h``[h:R]``h <> 0`` l ``0`` H1).
-Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros.
-Elim (H2 eps H3); Intros.
-Exists x0.
-Elim H4; Intros.
-Split.
-Assumption.
-Intros; Rewrite H0; Apply H6; Assumption.
-Intro; Unfold Rdiv; Ring.
-Qed.
-
-Lemma derivable_pt_lim_minus : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (minus_fct f1 f2) x ``l1-l2``).
-Intros.
-Apply unicite_step3.
-Assert H1 := (unicite_step2 ? ? ? H).
-Assert H2 := (unicite_step2 ? ? ? H0).
-Unfold  minus_fct.
-Cut (h:R)``((f1 (x+h))-(f1 x))/h-((f2 (x+h))-(f2 x))/h``==``((f1 (x+h))-(f2 (x+h))-((f1 x)-(f2 x)))/h``.
-Intro.
-Generalize (limit_minus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2).
-Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros.
-Elim (H4 eps H5); Intros.
-Exists x0.
-Elim H6; Intros.
-Split.
-Assumption.
-Intros; Rewrite <- H3; Apply H8; Assumption.
-Intro; Unfold Rdiv; Ring.
-Qed.
-
-Lemma derivable_pt_lim_mult : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (mult_fct f1 f2) x ``l1*(f2 x)+(f1 x)*l2``).
-Intros.
-Assert H1 := (derivable_pt_lim_D_in f1 [y:R]l1 x).
-Elim H1; Intros.
-Assert H4 := (H3 H).
-Assert H5 := (derivable_pt_lim_D_in f2 [y:R]l2 x).
-Elim H5; Intros.
-Assert H8 := (H7 H0).
-Clear H1 H2 H3 H5 H6 H7.
-Assert H1 := (derivable_pt_lim_D_in (mult_fct f1 f2) [y:R]``l1*(f2 x)+(f1 x)*l2`` x).
-Elim H1; Intros.
-Clear H1 H3.
-Apply H2.
-Unfold mult_fct.
-Apply (Dmult no_cond [y:R]l1 [y:R]l2 f1 f2 x); Assumption.
-Qed.
-
-Lemma derivable_pt_lim_const : (a,x:R) (derivable_pt_lim (fct_cte a) x ``0``).
-Intros; Unfold fct_cte derivable_pt_lim.
-Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Unfold Rminus; Rewrite Rplus_Ropp_r; Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
-Qed.
-
-Lemma derivable_pt_lim_scal : (f:R->R;a,x,l:R) (derivable_pt_lim f x l) -> (derivable_pt_lim (mult_real_fct a f) x ``a*l``).
-Intros.
-Assert H0 := (derivable_pt_lim_const a x).
-Replace (mult_real_fct a f) with (mult_fct (fct_cte a) f).
-Replace ``a*l`` with ``0*(f x)+a*l``; [Idtac | Ring].
-Apply (derivable_pt_lim_mult (fct_cte a) f x ``0`` l); Assumption.
-Unfold mult_real_fct mult_fct fct_cte; Reflexivity.
-Qed.
-
-Lemma derivable_pt_lim_id : (x:R) (derivable_pt_lim id x ``1``).
-Intro; Unfold derivable_pt_lim.
-Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Unfold id; Replace ``(x+h-x)/h-1`` with ``0``.
-Rewrite Rabsolu_R0; Apply Rle_lt_trans with ``(Rabsolu h)``.
-Apply Rabsolu_pos.
-Assumption.
-Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc.
-Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym.
-Symmetry; Apply Rplus_Ropp_r.
-Assumption.
-Qed.
-
-Lemma derivable_pt_lim_Rsqr : (x:R) (derivable_pt_lim Rsqr x ``2*x``).
-Intro; Unfold derivable_pt_lim.
-Unfold Rsqr; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``.
-Assumption.
-Replace ``(x+h)*(x+h)-x*x`` with ``2*x*h+h*h``; [Idtac | Ring].
-Unfold Rdiv; Rewrite Rmult_Rplus_distrl.
-Repeat Rewrite Rmult_assoc.
-Repeat Rewrite <- Rinv_r_sym; [Idtac | Assumption].
-Ring.
-Qed.
-
-Lemma derivable_pt_lim_comp : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 (f1 x) l2) -> (derivable_pt_lim (comp f2 f1) x ``l2*l1``).
-Intros; Assert H1 := (derivable_pt_lim_D_in f1 [y:R]l1 x).
-Elim H1; Intros.
-Assert H4 := (H3 H).
-Assert H5 := (derivable_pt_lim_D_in f2 [y:R]l2 (f1 x)).
-Elim H5; Intros.
-Assert H8 := (H7 H0).
-Clear H1 H2 H3 H5 H6 H7.
-Assert H1 := (derivable_pt_lim_D_in (comp f2 f1) [y:R]``l2*l1`` x).
-Elim H1; Intros.
-Clear H1 H3; Apply H2.
-Unfold comp; Cut (D_in [x0:R](f2 (f1 x0)) [y:R]``l2*l1`` (Dgf no_cond no_cond f1) x) -> (D_in [x0:R](f2 (f1 x0)) [y:R]``l2*l1`` no_cond x).
-Intro; Apply H1.
-Rewrite Rmult_sym; Apply (Dcomp no_cond no_cond [y:R]l1 [y:R]l2 f1 f2 x); Assumption.
-Unfold Dgf D_in no_cond; Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros.
-Elim (H1 eps H3); Intros.
-Exists x0; Intros; Split.
-Elim H5; Intros; Assumption.
-Intros; Elim H5; Intros; Apply H9; Split.
-Unfold D_x; Split.
-Split; Trivial.
-Elim H6; Intros; Unfold D_x in H10; Elim H10; Intros; Assumption.
-Elim H6; Intros; Assumption.
-Qed.
-
-Lemma derivable_pt_plus : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt (plus_fct f1 f2) x).
-Unfold derivable_pt; Intros.
-Elim X; Intros.
-Elim X0; Intros.
-Apply Specif.existT with ``x0+x1``.
-Apply derivable_pt_lim_plus; Assumption.
-Qed.
-
-Lemma derivable_pt_opp : (f:R->R;x:R) (derivable_pt f x) -> (derivable_pt (opp_fct f) x).
-Unfold derivable_pt; Intros.
-Elim X; Intros.
-Apply Specif.existT with ``-x0``.
-Apply derivable_pt_lim_opp; Assumption.
-Qed.
-
-Lemma derivable_pt_minus : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt (minus_fct f1 f2) x).
-Unfold derivable_pt; Intros.
-Elim X; Intros.
-Elim X0; Intros.
-Apply Specif.existT with ``x0-x1``.
-Apply derivable_pt_lim_minus; Assumption.
-Qed.
-
-Lemma derivable_pt_mult : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt (mult_fct f1 f2) x).
-Unfold derivable_pt; Intros.
-Elim X; Intros.
-Elim X0; Intros.
-Apply Specif.existT with ``x0*(f2 x)+(f1 x)*x1``.
-Apply derivable_pt_lim_mult; Assumption.
-Qed.
-
-Lemma derivable_pt_const : (a,x:R) (derivable_pt (fct_cte a) x).
-Intros; Unfold derivable_pt.
-Apply Specif.existT with ``0``.
-Apply derivable_pt_lim_const.
-Qed.
-
-Lemma derivable_pt_scal : (f:R->R;a,x:R) (derivable_pt f x) -> (derivable_pt (mult_real_fct a f) x).
-Unfold derivable_pt; Intros.
-Elim X; Intros.
-Apply Specif.existT with ``a*x0``.
-Apply derivable_pt_lim_scal; Assumption.
-Qed.
-
-Lemma derivable_pt_id : (x:R) (derivable_pt id x).
-Unfold derivable_pt; Intro.
-Exists ``1``.
-Apply derivable_pt_lim_id.
-Qed.
-
-Lemma derivable_pt_Rsqr : (x:R) (derivable_pt Rsqr x).
-Unfold derivable_pt; Intro; Apply Specif.existT with ``2*x``.
-Apply derivable_pt_lim_Rsqr.
-Qed.
-
-Lemma derivable_pt_comp : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 (f1 x)) -> (derivable_pt (comp f2 f1) x).
-Unfold derivable_pt; Intros.
-Elim X; Intros.
-Elim X0 ;Intros.
-Apply Specif.existT with ``x1*x0``.
-Apply derivable_pt_lim_comp; Assumption.
-Qed.
-
-Lemma derivable_plus : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (plus_fct f1 f2)).
-Unfold derivable; Intros.
-Apply (derivable_pt_plus ? ? x (X ?) (X0 ?)).
-Qed.
-
-Lemma derivable_opp : (f:R->R) (derivable f) -> (derivable (opp_fct f)).
-Unfold derivable; Intros.
-Apply (derivable_pt_opp ? x (X ?)).
-Qed.
-
-Lemma derivable_minus : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (minus_fct f1 f2)).
-Unfold derivable; Intros.
-Apply (derivable_pt_minus ? ? x (X ?) (X0 ?)).
-Qed.
-
-Lemma derivable_mult : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (mult_fct f1 f2)).
-Unfold derivable; Intros.
-Apply (derivable_pt_mult ? ? x (X ?) (X0 ?)).
-Qed.
-
-Lemma derivable_const : (a:R) (derivable (fct_cte a)).
-Unfold derivable; Intros.
-Apply derivable_pt_const.
-Qed.
-
-Lemma derivable_scal : (f:R->R;a:R) (derivable f) -> (derivable (mult_real_fct a f)).
-Unfold derivable; Intros.
-Apply (derivable_pt_scal ? a x (X ?)).
-Qed.
-
-Lemma derivable_id : (derivable id).
-Unfold derivable; Intro; Apply derivable_pt_id.
-Qed.
-
-Lemma derivable_Rsqr : (derivable Rsqr).
-Unfold derivable; Intro; Apply derivable_pt_Rsqr.
-Qed.
-
-Lemma derivable_comp : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (comp f2 f1)).
-Unfold derivable; Intros.
-Apply (derivable_pt_comp ? ? x (X ?) (X0 ?)).
-Qed.
-
-Lemma derive_pt_plus : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 x)) ``(derive_pt (plus_fct f1 f2) x (derivable_pt_plus ? ? ? pr1 pr2)) == (derive_pt f1 x pr1) + (derive_pt f2 x pr2)``.
-Intros.
-Assert H := (derivable_derive f1 x pr1).
-Assert H0 := (derivable_derive f2 x pr2).
-Assert H1 := (derivable_derive (plus_fct f1 f2) x (derivable_pt_plus ? ? ? pr1 pr2)).
-Elim H; Clear H; Intros l1 H.
-Elim H0; Clear H0; Intros l2 H0.
-Elim H1; Clear H1; Intros l H1.
-Rewrite H; Rewrite H0; Apply derive_pt_eq_0.
-Assert H3 := (projT2 ? ? pr1).
-Unfold derive_pt in H; Rewrite H in H3.
-Assert H4 := (projT2 ? ? pr2).
-Unfold derive_pt in H0; Rewrite H0 in H4.
-Apply derivable_pt_lim_plus; Assumption.
-Qed.
-
-Lemma derive_pt_opp : (f:R->R;x:R;pr1:(derivable_pt f x)) ``(derive_pt (opp_fct f) x (derivable_pt_opp ? ? pr1)) == -(derive_pt f x pr1)``.
-Intros.
-Assert H := (derivable_derive f x pr1).
-Assert H0 := (derivable_derive (opp_fct f) x (derivable_pt_opp ? ? pr1)).
-Elim H; Clear H; Intros l1 H.
-Elim H0; Clear H0; Intros l2 H0.
-Rewrite H; Apply derive_pt_eq_0.
-Assert H3 := (projT2 ? ? pr1).
-Unfold derive_pt in H; Rewrite H in H3.
-Apply derivable_pt_lim_opp; Assumption.
-Qed.
-
-Lemma derive_pt_minus : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 x)) ``(derive_pt (minus_fct f1 f2) x (derivable_pt_minus ? ? ? pr1 pr2)) == (derive_pt f1 x pr1) - (derive_pt f2 x pr2)``.
-Intros.
-Assert H := (derivable_derive f1 x pr1).
-Assert H0 := (derivable_derive f2 x pr2).
-Assert H1 := (derivable_derive (minus_fct f1 f2) x (derivable_pt_minus ? ? ? pr1 pr2)).
-Elim H; Clear H; Intros l1 H.
-Elim H0; Clear H0; Intros l2 H0.
-Elim H1; Clear H1; Intros l H1.
-Rewrite H; Rewrite H0; Apply derive_pt_eq_0.
-Assert H3 := (projT2 ? ? pr1).
-Unfold derive_pt in H; Rewrite H in H3.
-Assert H4 := (projT2 ? ? pr2).
-Unfold derive_pt in H0; Rewrite H0 in H4.
-Apply derivable_pt_lim_minus; Assumption.
-Qed.
-
-Lemma derive_pt_mult : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 x)) ``(derive_pt (mult_fct f1 f2) x (derivable_pt_mult ? ? ? pr1 pr2)) == (derive_pt f1 x pr1)*(f2 x) + (f1 x)*(derive_pt f2 x pr2)``.
-Intros.
-Assert H := (derivable_derive f1 x pr1).
-Assert H0 := (derivable_derive f2 x pr2).
-Assert H1 := (derivable_derive (mult_fct f1 f2) x (derivable_pt_mult ? ? ? pr1 pr2)).
-Elim H; Clear H; Intros l1 H.
-Elim H0; Clear H0; Intros l2 H0.
-Elim H1; Clear H1; Intros l H1.
-Rewrite H; Rewrite H0; Apply derive_pt_eq_0.
-Assert H3 := (projT2 ? ? pr1).
-Unfold derive_pt in H; Rewrite H in H3.
-Assert H4 := (projT2 ? ? pr2).
-Unfold derive_pt in H0; Rewrite H0 in H4.
-Apply derivable_pt_lim_mult; Assumption.
-Qed.
-
-Lemma derive_pt_const : (a,x:R) (derive_pt (fct_cte a) x (derivable_pt_const a x)) == R0.
-Intros.
-Apply derive_pt_eq_0.
-Apply derivable_pt_lim_const.
-Qed.
-
-Lemma derive_pt_scal : (f:R->R;a,x:R;pr:(derivable_pt f x)) ``(derive_pt (mult_real_fct a f) x (derivable_pt_scal ? ? ? pr)) == a * (derive_pt f x pr)``.
-Intros.
-Assert H := (derivable_derive f x pr).
-Assert H0 := (derivable_derive (mult_real_fct a f) x (derivable_pt_scal ? ? ? pr)).
-Elim H; Clear H; Intros l1 H.
-Elim H0; Clear H0; Intros l2 H0.
-Rewrite H; Apply derive_pt_eq_0.
-Assert H3 := (projT2 ? ? pr).
-Unfold derive_pt in H; Rewrite H in H3.
-Apply derivable_pt_lim_scal; Assumption.
-Qed.
-
-Lemma derive_pt_id : (x:R) (derive_pt id x (derivable_pt_id ?))==R1.
-Intros.
-Apply derive_pt_eq_0.
-Apply derivable_pt_lim_id.
-Qed.
-
-Lemma derive_pt_Rsqr : (x:R) (derive_pt Rsqr x (derivable_pt_Rsqr ?)) == ``2*x``.
-Intros.
-Apply derive_pt_eq_0.
-Apply derivable_pt_lim_Rsqr.
-Qed.
-
-Lemma derive_pt_comp : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 (f1 x))) ``(derive_pt (comp f2 f1) x (derivable_pt_comp ? ? ? pr1 pr2)) == (derive_pt f2 (f1 x) pr2) * (derive_pt f1 x pr1)``.
-Intros.
-Assert H := (derivable_derive f1 x pr1).
-Assert H0 := (derivable_derive f2 (f1 x) pr2).
-Assert H1 := (derivable_derive (comp f2 f1) x (derivable_pt_comp ? ? ? pr1 pr2)).
-Elim H; Clear H; Intros l1 H.
-Elim H0; Clear H0; Intros l2 H0.
-Elim H1; Clear H1; Intros l H1.
-Rewrite H; Rewrite H0; Apply derive_pt_eq_0.
-Assert H3 := (projT2 ? ? pr1).
-Unfold derive_pt in H; Rewrite H in H3.
-Assert H4 := (projT2 ? ? pr2).
-Unfold derive_pt in H0; Rewrite H0 in H4.
-Apply derivable_pt_lim_comp; Assumption.
+Lemma derivable_pt_lim_plus :
+ forall f1 f2 (x l1 l2:R),
+   derivable_pt_lim f1 x l1 ->
+   derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 + f2) x (l1 + l2).
+intros.
+apply uniqueness_step3.
+assert (H1 := uniqueness_step2 _ _ _ H).
+assert (H2 := uniqueness_step2 _ _ _ H0).
+unfold plus_fct in |- *.
+cut
+ (forall h:R,
+    (f1 (x + h) + f2 (x + h) - (f1 x + f2 x)) / h =
+    (f1 (x + h) - f1 x) / h + (f2 (x + h) - f2 x) / h).
+intro.
+generalize
+ (limit_plus (fun h':R => (f1 (x + h') - f1 x) / h')
+    (fun h':R => (f2 (x + h') - f2 x) / h') (fun h:R => h <> 0) l1 l2 0 H1 H2).
+unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
+ simpl in |- *; unfold R_dist in |- *; intros.
+elim (H4 eps H5); intros.
+exists x0.
+elim H6; intros.
+split.
+assumption.
+intros; rewrite H3; apply H8; assumption.
+intro; unfold Rdiv in |- *; ring.
+Qed.
+
+Lemma derivable_pt_lim_opp :
+ forall f (x l:R), derivable_pt_lim f x l -> derivable_pt_lim (- f) x (- l).
+intros.
+apply uniqueness_step3.
+assert (H1 := uniqueness_step2 _ _ _ H).
+unfold opp_fct in |- *.
+cut (forall h:R, (- f (x + h) - - f x) / h = - ((f (x + h) - f x) / h)).
+intro.
+generalize
+ (limit_Ropp (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0 H1).
+unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
+ simpl in |- *; unfold R_dist in |- *; intros.
+elim (H2 eps H3); intros.
+exists x0.
+elim H4; intros.
+split.
+assumption.
+intros; rewrite H0; apply H6; assumption.
+intro; unfold Rdiv in |- *; ring.
+Qed.
+
+Lemma derivable_pt_lim_minus :
+ forall f1 f2 (x l1 l2:R),
+   derivable_pt_lim f1 x l1 ->
+   derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 - f2) x (l1 - l2).
+intros.
+apply uniqueness_step3.
+assert (H1 := uniqueness_step2 _ _ _ H).
+assert (H2 := uniqueness_step2 _ _ _ H0).
+unfold minus_fct in |- *.
+cut
+ (forall h:R,
+    (f1 (x + h) - f1 x) / h - (f2 (x + h) - f2 x) / h =
+    (f1 (x + h) - f2 (x + h) - (f1 x - f2 x)) / h).
+intro.
+generalize
+ (limit_minus (fun h':R => (f1 (x + h') - f1 x) / h')
+    (fun h':R => (f2 (x + h') - f2 x) / h') (fun h:R => h <> 0) l1 l2 0 H1 H2).
+unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *;
+ simpl in |- *; unfold R_dist in |- *; intros.
+elim (H4 eps H5); intros.
+exists x0.
+elim H6; intros.
+split.
+assumption.
+intros; rewrite <- H3; apply H8; assumption.
+intro; unfold Rdiv in |- *; ring.
+Qed.
+
+Lemma derivable_pt_lim_mult :
+ forall f1 f2 (x l1 l2:R),
+   derivable_pt_lim f1 x l1 ->
+   derivable_pt_lim f2 x l2 ->
+   derivable_pt_lim (f1 * f2) x (l1 * f2 x + f1 x * l2).
+intros.
+assert (H1 := derivable_pt_lim_D_in f1 (fun y:R => l1) x).
+elim H1; intros.
+assert (H4 := H3 H).
+assert (H5 := derivable_pt_lim_D_in f2 (fun y:R => l2) x).
+elim H5; intros.
+assert (H8 := H7 H0).
+clear H1 H2 H3 H5 H6 H7.
+assert
+ (H1 :=
+  derivable_pt_lim_D_in (f1 * f2)%F (fun y:R => l1 * f2 x + f1 x * l2) x).
+elim H1; intros.
+clear H1 H3.
+apply H2.
+unfold mult_fct in |- *.
+apply (Dmult no_cond (fun y:R => l1) (fun y:R => l2) f1 f2 x); assumption.
+Qed.
+
+Lemma derivable_pt_lim_const : forall a x:R, derivable_pt_lim (fct_cte a) x 0.
+intros; unfold fct_cte, derivable_pt_lim in |- *.
+intros; exists (mkposreal 1 Rlt_0_1); intros; unfold Rminus in |- *;
+ rewrite Rplus_opp_r; unfold Rdiv in |- *; rewrite Rmult_0_l;
+ rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
+Qed.
+
+Lemma derivable_pt_lim_scal :
+ forall f (a x l:R),
+   derivable_pt_lim f x l -> derivable_pt_lim (mult_real_fct a f) x (a * l).
+intros.
+assert (H0 := derivable_pt_lim_const a x).
+replace (mult_real_fct a f) with (fct_cte a * f)%F.
+replace (a * l) with (0 * f x + a * l); [ idtac | ring ].
+apply (derivable_pt_lim_mult (fct_cte a) f x 0 l); assumption.
+unfold mult_real_fct, mult_fct, fct_cte in |- *; reflexivity.
+Qed.
+
+Lemma derivable_pt_lim_id : forall x:R, derivable_pt_lim id x 1.
+intro; unfold derivable_pt_lim in |- *.
+intros eps Heps; exists (mkposreal eps Heps); intros h H1 H2;
+ unfold id in |- *; replace ((x + h - x) / h - 1) with 0.
+rewrite Rabs_R0; apply Rle_lt_trans with (Rabs h).
+apply Rabs_pos.
+assumption.
+unfold Rminus in |- *; rewrite Rplus_assoc; rewrite (Rplus_comm x);
+ rewrite Rplus_assoc.
+rewrite Rplus_opp_l; rewrite Rplus_0_r; unfold Rdiv in |- *;
+ rewrite <- Rinv_r_sym.
+symmetry  in |- *; apply Rplus_opp_r.
+assumption.
+Qed.
+
+Lemma derivable_pt_lim_Rsqr : forall x:R, derivable_pt_lim Rsqr x (2 * x).
+intro; unfold derivable_pt_lim in |- *.
+unfold Rsqr in |- *; intros eps Heps; exists (mkposreal eps Heps);
+ intros h H1 H2; replace (((x + h) * (x + h) - x * x) / h - 2 * x) with h.
+assumption.
+replace ((x + h) * (x + h) - x * x) with (2 * x * h + h * h);
+ [ idtac | ring ].
+unfold Rdiv in |- *; rewrite Rmult_plus_distr_r.
+repeat rewrite Rmult_assoc.
+repeat rewrite <- Rinv_r_sym; [ idtac | assumption ].
+ring.
+Qed.
+
+Lemma derivable_pt_lim_comp :
+ forall f1 f2 (x l1 l2:R),
+   derivable_pt_lim f1 x l1 ->
+   derivable_pt_lim f2 (f1 x) l2 -> derivable_pt_lim (f2 o f1) x (l2 * l1).
+intros; assert (H1 := derivable_pt_lim_D_in f1 (fun y:R => l1) x).
+elim H1; intros.
+assert (H4 := H3 H).
+assert (H5 := derivable_pt_lim_D_in f2 (fun y:R => l2) (f1 x)).
+elim H5; intros.
+assert (H8 := H7 H0).
+clear H1 H2 H3 H5 H6 H7.
+assert (H1 := derivable_pt_lim_D_in (f2 o f1)%F (fun y:R => l2 * l1) x).
+elim H1; intros.
+clear H1 H3; apply H2.
+unfold comp in |- *;
+ cut
+  (D_in (fun x0:R => f2 (f1 x0)) (fun y:R => l2 * l1)
+     (Dgf no_cond no_cond f1) x ->
+   D_in (fun x0:R => f2 (f1 x0)) (fun y:R => l2 * l1) no_cond x).
+intro; apply H1.
+rewrite Rmult_comm;
+ apply (Dcomp no_cond no_cond (fun y:R => l1) (fun y:R => l2) f1 f2 x);
+ assumption.
+unfold Dgf, D_in, no_cond in |- *; unfold limit1_in in |- *;
+ unfold limit_in in |- *; unfold dist in |- *; simpl in |- *;
+ unfold R_dist in |- *; intros.
+elim (H1 eps H3); intros.
+exists x0; intros; split.
+elim H5; intros; assumption.
+intros; elim H5; intros; apply H9; split.
+unfold D_x in |- *; split.
+split; trivial.
+elim H6; intros; unfold D_x in H10; elim H10; intros; assumption.
+elim H6; intros; assumption.
+Qed.
+
+Lemma derivable_pt_plus :
+ forall f1 f2 (x:R),
+   derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 + f2) x.
+unfold derivable_pt in |- *; intros.
+elim X; intros.
+elim X0; intros.
+apply existT with (x0 + x1).
+apply derivable_pt_lim_plus; assumption.
+Qed.
+
+Lemma derivable_pt_opp :
+ forall f (x:R), derivable_pt f x -> derivable_pt (- f) x.
+unfold derivable_pt in |- *; intros.
+elim X; intros.
+apply existT with (- x0).
+apply derivable_pt_lim_opp; assumption.
+Qed.
+
+Lemma derivable_pt_minus :
+ forall f1 f2 (x:R),
+   derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 - f2) x.
+unfold derivable_pt in |- *; intros.
+elim X; intros.
+elim X0; intros.
+apply existT with (x0 - x1).
+apply derivable_pt_lim_minus; assumption.
+Qed.
+
+Lemma derivable_pt_mult :
+ forall f1 f2 (x:R),
+   derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 * f2) x.
+unfold derivable_pt in |- *; intros.
+elim X; intros.
+elim X0; intros.
+apply existT with (x0 * f2 x + f1 x * x1).
+apply derivable_pt_lim_mult; assumption.
+Qed.
+
+Lemma derivable_pt_const : forall a x:R, derivable_pt (fct_cte a) x.
+intros; unfold derivable_pt in |- *.
+apply existT with 0.
+apply derivable_pt_lim_const.
+Qed.
+
+Lemma derivable_pt_scal :
+ forall f (a x:R), derivable_pt f x -> derivable_pt (mult_real_fct a f) x.
+unfold derivable_pt in |- *; intros.
+elim X; intros.
+apply existT with (a * x0).
+apply derivable_pt_lim_scal; assumption.
+Qed.
+
+Lemma derivable_pt_id : forall x:R, derivable_pt id x.
+unfold derivable_pt in |- *; intro.
+exists 1.
+apply derivable_pt_lim_id.
+Qed.
+
+Lemma derivable_pt_Rsqr : forall x:R, derivable_pt Rsqr x.
+unfold derivable_pt in |- *; intro; apply existT with (2 * x).
+apply derivable_pt_lim_Rsqr.
+Qed.
+
+Lemma derivable_pt_comp :
+ forall f1 f2 (x:R),
+   derivable_pt f1 x -> derivable_pt f2 (f1 x) -> derivable_pt (f2 o f1) x.
+unfold derivable_pt in |- *; intros.
+elim X; intros.
+elim X0; intros.
+apply existT with (x1 * x0).
+apply derivable_pt_lim_comp; assumption.
+Qed.
+
+Lemma derivable_plus :
+ forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 + f2).
+unfold derivable in |- *; intros.
+apply (derivable_pt_plus _ _ x (X _) (X0 _)).
+Qed.
+
+Lemma derivable_opp : forall f, derivable f -> derivable (- f).
+unfold derivable in |- *; intros.
+apply (derivable_pt_opp _ x (X _)).
+Qed.
+
+Lemma derivable_minus :
+ forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 - f2).
+unfold derivable in |- *; intros.
+apply (derivable_pt_minus _ _ x (X _) (X0 _)).
+Qed.
+
+Lemma derivable_mult :
+ forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 * f2).
+unfold derivable in |- *; intros.
+apply (derivable_pt_mult _ _ x (X _) (X0 _)).
+Qed.
+
+Lemma derivable_const : forall a:R, derivable (fct_cte a).
+unfold derivable in |- *; intros.
+apply derivable_pt_const.
+Qed.
+
+Lemma derivable_scal :
+ forall f (a:R), derivable f -> derivable (mult_real_fct a f).
+unfold derivable in |- *; intros.
+apply (derivable_pt_scal _ a x (X _)).
+Qed.
+
+Lemma derivable_id : derivable id.
+unfold derivable in |- *; intro; apply derivable_pt_id.
+Qed.
+
+Lemma derivable_Rsqr : derivable Rsqr.
+unfold derivable in |- *; intro; apply derivable_pt_Rsqr.
+Qed.
+
+Lemma derivable_comp :
+ forall f1 f2, derivable f1 -> derivable f2 -> derivable (f2 o f1).
+unfold derivable in |- *; intros.
+apply (derivable_pt_comp _ _ x (X _) (X0 _)).
+Qed.
+
+Lemma derive_pt_plus :
+ forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
+   derive_pt (f1 + f2) x (derivable_pt_plus _ _ _ pr1 pr2) =
+   derive_pt f1 x pr1 + derive_pt f2 x pr2.
+intros.
+assert (H := derivable_derive f1 x pr1).
+assert (H0 := derivable_derive f2 x pr2).
+assert
+ (H1 := derivable_derive (f1 + f2)%F x (derivable_pt_plus _ _ _ pr1 pr2)).
+elim H; clear H; intros l1 H.
+elim H0; clear H0; intros l2 H0.
+elim H1; clear H1; intros l H1.
+rewrite H; rewrite H0; apply derive_pt_eq_0.
+assert (H3 := projT2 pr1).
+unfold derive_pt in H; rewrite H in H3.
+assert (H4 := projT2 pr2).
+unfold derive_pt in H0; rewrite H0 in H4.
+apply derivable_pt_lim_plus; assumption.
+Qed.
+
+Lemma derive_pt_opp :
+ forall f (x:R) (pr1:derivable_pt f x),
+   derive_pt (- f) x (derivable_pt_opp _ _ pr1) = - derive_pt f x pr1.
+intros.
+assert (H := derivable_derive f x pr1).
+assert (H0 := derivable_derive (- f)%F x (derivable_pt_opp _ _ pr1)).
+elim H; clear H; intros l1 H.
+elim H0; clear H0; intros l2 H0.
+rewrite H; apply derive_pt_eq_0.
+assert (H3 := projT2 pr1).
+unfold derive_pt in H; rewrite H in H3.
+apply derivable_pt_lim_opp; assumption.
+Qed.
+
+Lemma derive_pt_minus :
+ forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
+   derive_pt (f1 - f2) x (derivable_pt_minus _ _ _ pr1 pr2) =
+   derive_pt f1 x pr1 - derive_pt f2 x pr2.
+intros.
+assert (H := derivable_derive f1 x pr1).
+assert (H0 := derivable_derive f2 x pr2).
+assert
+ (H1 := derivable_derive (f1 - f2)%F x (derivable_pt_minus _ _ _ pr1 pr2)).
+elim H; clear H; intros l1 H.
+elim H0; clear H0; intros l2 H0.
+elim H1; clear H1; intros l H1.
+rewrite H; rewrite H0; apply derive_pt_eq_0.
+assert (H3 := projT2 pr1).
+unfold derive_pt in H; rewrite H in H3.
+assert (H4 := projT2 pr2).
+unfold derive_pt in H0; rewrite H0 in H4.
+apply derivable_pt_lim_minus; assumption.
+Qed.
+
+Lemma derive_pt_mult :
+ forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
+   derive_pt (f1 * f2) x (derivable_pt_mult _ _ _ pr1 pr2) =
+   derive_pt f1 x pr1 * f2 x + f1 x * derive_pt f2 x pr2.
+intros.
+assert (H := derivable_derive f1 x pr1).
+assert (H0 := derivable_derive f2 x pr2).
+assert
+ (H1 := derivable_derive (f1 * f2)%F x (derivable_pt_mult _ _ _ pr1 pr2)).
+elim H; clear H; intros l1 H.
+elim H0; clear H0; intros l2 H0.
+elim H1; clear H1; intros l H1.
+rewrite H; rewrite H0; apply derive_pt_eq_0.
+assert (H3 := projT2 pr1).
+unfold derive_pt in H; rewrite H in H3.
+assert (H4 := projT2 pr2).
+unfold derive_pt in H0; rewrite H0 in H4.
+apply derivable_pt_lim_mult; assumption.
+Qed.
+
+Lemma derive_pt_const :
+ forall a x:R, derive_pt (fct_cte a) x (derivable_pt_const a x) = 0.
+intros.
+apply derive_pt_eq_0.
+apply derivable_pt_lim_const.
+Qed.
+
+Lemma derive_pt_scal :
+ forall f (a x:R) (pr:derivable_pt f x),
+   derive_pt (mult_real_fct a f) x (derivable_pt_scal _ _ _ pr) =
+   a * derive_pt f x pr.
+intros.
+assert (H := derivable_derive f x pr).
+assert
+ (H0 := derivable_derive (mult_real_fct a f) x (derivable_pt_scal _ _ _ pr)).
+elim H; clear H; intros l1 H.
+elim H0; clear H0; intros l2 H0.
+rewrite H; apply derive_pt_eq_0.
+assert (H3 := projT2 pr).
+unfold derive_pt in H; rewrite H in H3.
+apply derivable_pt_lim_scal; assumption.
+Qed.
+
+Lemma derive_pt_id : forall x:R, derive_pt id x (derivable_pt_id _) = 1.
+intros.
+apply derive_pt_eq_0.
+apply derivable_pt_lim_id.
+Qed.
+
+Lemma derive_pt_Rsqr :
+ forall x:R, derive_pt Rsqr x (derivable_pt_Rsqr _) = 2 * x.
+intros.
+apply derive_pt_eq_0.
+apply derivable_pt_lim_Rsqr.
+Qed.
+
+Lemma derive_pt_comp :
+ forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 (f1 x)),
+   derive_pt (f2 o f1) x (derivable_pt_comp _ _ _ pr1 pr2) =
+   derive_pt f2 (f1 x) pr2 * derive_pt f1 x pr1.
+intros.
+assert (H := derivable_derive f1 x pr1).
+assert (H0 := derivable_derive f2 (f1 x) pr2).
+assert
+ (H1 := derivable_derive (f2 o f1)%F x (derivable_pt_comp _ _ _ pr1 pr2)).
+elim H; clear H; intros l1 H.
+elim H0; clear H0; intros l2 H0.
+elim H1; clear H1; intros l H1.
+rewrite H; rewrite H0; apply derive_pt_eq_0.
+assert (H3 := projT2 pr1).
+unfold derive_pt in H; rewrite H in H3.
+assert (H4 := projT2 pr2).
+unfold derive_pt in H0; rewrite H0 in H4.
+apply derivable_pt_lim_comp; assumption.
 Qed.
 
 (* Pow *)
-Definition pow_fct [n:nat] : R->R := [y:R](pow y n).
-
-Lemma derivable_pt_lim_pow_pos : (x:R;n:nat) (lt O n) -> (derivable_pt_lim [y:R](pow y n) x ``(INR n)*(pow x (pred n))``).
-Intros.
-Induction n.
-Elim (lt_n_n ? H).
-Cut n=O\/(lt O n).
-Intro; Elim H0; Intro.
-Rewrite H1; Simpl.
-Replace [y:R]``y*1`` with (mult_fct id (fct_cte R1)).
-Replace ``1*1`` with ``1*(fct_cte R1 x)+(id x)*0``.
-Apply derivable_pt_lim_mult.
-Apply derivable_pt_lim_id.
-Apply derivable_pt_lim_const.
-Unfold fct_cte id; Ring.
-Reflexivity.
-Replace [y:R](pow y (S n)) with [y:R]``y*(pow y n)``.
-Replace (pred (S n)) with n; [Idtac | Reflexivity].
-Replace [y:R]``y*(pow y n)`` with (mult_fct id [y:R](pow y n)).
-Pose f := [y:R](pow y n).
-Replace ``(INR (S n))*(pow x n)`` with (Rplus (Rmult R1 (f x)) (Rmult (id x) (Rmult (INR n) (pow x (pred n))))).
-Apply derivable_pt_lim_mult.
-Apply derivable_pt_lim_id.
-Unfold f; Apply Hrecn; Assumption.
-Unfold f.
-Pattern 1 5 n; Replace n with (S (pred n)).
-Unfold id; Rewrite S_INR; Simpl.
-Ring.
-Symmetry; Apply S_pred with O; Assumption.
-Unfold mult_fct id; Reflexivity.
-Reflexivity.
-Inversion H.
-Left; Reflexivity.
-Right.
-Apply lt_le_trans with (1).
-Apply lt_O_Sn.
-Assumption.
-Qed.
-
-Lemma derivable_pt_lim_pow : (x:R; n:nat) (derivable_pt_lim [y:R](pow y n) x ``(INR n)*(pow x (pred n))``).
-Intros.
-Induction n.
-Simpl.
-Rewrite Rmult_Ol.
-Replace [_:R]``1`` with (fct_cte R1); [Apply derivable_pt_lim_const | Reflexivity].
-Apply derivable_pt_lim_pow_pos.
-Apply lt_O_Sn.
-Qed.
-
-Lemma derivable_pt_pow : (n:nat;x:R) (derivable_pt [y:R](pow y n) x).
-Intros; Unfold derivable_pt.
-Apply Specif.existT with ``(INR n)*(pow x (pred n))``.
-Apply derivable_pt_lim_pow.
-Qed.
-
-Lemma derivable_pow : (n:nat) (derivable [y:R](pow y n)).
-Intro; Unfold derivable; Intro; Apply derivable_pt_pow.
-Qed.
-
-Lemma derive_pt_pow : (n:nat;x:R) (derive_pt [y:R](pow y n) x (derivable_pt_pow n x))==``(INR n)*(pow x (pred n))``.
-Intros; Apply derive_pt_eq_0.
-Apply derivable_pt_lim_pow.
-Qed.
-
-Lemma pr_nu : (f:R->R;x:R;pr1,pr2:(derivable_pt f x)) (derive_pt f x pr1)==(derive_pt f x pr2). 
-Intros.
-Unfold derivable_pt in pr1.
-Unfold derivable_pt in pr2.
-Elim pr1; Intros.
-Elim pr2; Intros.
-Unfold derivable_pt_abs in p.
-Unfold derivable_pt_abs in p0.
-Simpl.
-Apply (unicite_limite f x x0 x1 p p0).
+Definition pow_fct (n:nat) (y:R) : R := y ^ n.
+
+Lemma derivable_pt_lim_pow_pos :
+ forall (x:R) (n:nat),
+   (0 < n)%nat -> derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).
+intros.
+induction  n as [| n Hrecn].
+elim (lt_irrefl _ H).
+cut (n = 0%nat \/ (0 < n)%nat).
+intro; elim H0; intro.
+rewrite H1; simpl in |- *.
+replace (fun y:R => y * 1) with (id * fct_cte 1)%F.
+replace (1 * 1) with (1 * fct_cte 1 x + id x * 0).
+apply derivable_pt_lim_mult.
+apply derivable_pt_lim_id.
+apply derivable_pt_lim_const.
+unfold fct_cte, id in |- *; ring.
+reflexivity.
+replace (fun y:R => y ^ S n) with (fun y:R => y * y ^ n).
+replace (pred (S n)) with n; [ idtac | reflexivity ].
+replace (fun y:R => y * y ^ n) with (id * (fun y:R => y ^ n))%F.
+pose (f := fun y:R => y ^ n).
+replace (INR (S n) * x ^ n) with (1 * f x + id x * (INR n * x ^ pred n)).
+apply derivable_pt_lim_mult.
+apply derivable_pt_lim_id.
+unfold f in |- *; apply Hrecn; assumption.
+unfold f in |- *.
+pattern n at 1 5 in |- *; replace n with (S (pred n)).
+unfold id in |- *; rewrite S_INR; simpl in |- *.
+ring.
+symmetry  in |- *; apply S_pred with 0%nat; assumption.
+unfold mult_fct, id in |- *; reflexivity.
+reflexivity.
+inversion H.
+left; reflexivity.
+right.
+apply lt_le_trans with 1%nat.
+apply lt_O_Sn.
+assumption.
+Qed.
+
+Lemma derivable_pt_lim_pow :
+ forall (x:R) (n:nat),
+   derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).
+intros.
+induction  n as [| n Hrecn].
+simpl in |- *.
+rewrite Rmult_0_l.
+replace (fun _:R => 1) with (fct_cte 1);
+ [ apply derivable_pt_lim_const | reflexivity ].
+apply derivable_pt_lim_pow_pos.
+apply lt_O_Sn.
+Qed.
+
+Lemma derivable_pt_pow :
+ forall (n:nat) (x:R), derivable_pt (fun y:R => y ^ n) x.
+intros; unfold derivable_pt in |- *.
+apply existT with (INR n * x ^ pred n).
+apply derivable_pt_lim_pow.
+Qed.
+
+Lemma derivable_pow : forall n:nat, derivable (fun y:R => y ^ n).
+intro; unfold derivable in |- *; intro; apply derivable_pt_pow.
+Qed.
+
+Lemma derive_pt_pow :
+ forall (n:nat) (x:R),
+   derive_pt (fun y:R => y ^ n) x (derivable_pt_pow n x) = INR n * x ^ pred n.
+intros; apply derive_pt_eq_0.
+apply derivable_pt_lim_pow.
+Qed.
+
+Lemma pr_nu :
+ forall f (x:R) (pr1 pr2:derivable_pt f x),
+   derive_pt f x pr1 = derive_pt f x pr2. 
+intros.
+unfold derivable_pt in pr1.
+unfold derivable_pt in pr2.
+elim pr1; intros.
+elim pr2; intros.
+unfold derivable_pt_abs in p.
+unfold derivable_pt_abs in p0.
+simpl in |- *.
+apply (uniqueness_limite f x x0 x1 p p0).
 Qed.
 
 
@@ -787,260 +1001,479 @@ Qed.
 (**             Local extremum's condition                  *)
 (************************************************************)
 
-Theorem deriv_maximum : (f:R->R;a,b,c:R;pr:(derivable_pt f c)) ``a<c``->``c<b``->((x:R) ``a<x``->``x<b``->``(f x)<=(f c)``)->``(derive_pt f c pr)==0``.
-Intros; Case (total_order R0 (derive_pt f c pr)); Intro.
-Assert H3 := (derivable_derive f c pr).
-Elim H3; Intros l H4; Rewrite H4 in H2.
-Assert H5 := (derive_pt_eq_1 f c l pr H4).
-Cut ``0<l/2``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]].
-Elim (H5 ``l/2`` H6); Intros delta H7.
-Cut ``0<(b-c)/2``.
-Intro; Cut ``(Rmin delta/2 ((b-c)/2))<>0``.
-Intro; Cut ``(Rabsolu (Rmin delta/2 ((b-c)/2)))<delta``.
-Intro.
-Assert H11 := (H7 ``(Rmin delta/2 ((b-c)/2))`` H9 H10).
-Cut ``0<(Rmin (delta/2) ((b-c)/2))``.
-Intro; Cut ``a<c+(Rmin (delta/2) ((b-c)/2))``.
-Intro; Cut ``c+(Rmin (delta/2) ((b-c)/2))<b``.
-Intro; Assert H15 := (H1 ``c+(Rmin (delta/2) ((b-c)/2))`` H13 H14).
-Cut ``((f (c+(Rmin (delta/2) ((b-c)/2))))-(f c))/(Rmin (delta/2) ((b-c)/2))<=0``.
-Intro; Cut ``-l<0``.
-Intro; Unfold Rminus in H11.
-Cut ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l<0``.
-Intro; Cut ``(Rabsolu (((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l)) < l/2``.
-Unfold Rabsolu; Case (case_Rabsolu ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l``); Intro.
-Replace `` -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l)`` with ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))``.
-Intro; Generalize (Rlt_compatibility ``-l`` ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``l/2`` H19); Repeat Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Replace ``-l+l/2`` with ``-(l/2)``.
-Intro; Generalize (Rlt_Ropp ``-(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``-(l/2)`` H20); Repeat Rewrite Ropp_Ropp; Intro; Generalize (Rlt_trans ``0`` ``l/2`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` H6 H21); Intro; Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` ``0`` H22 H16)).
-Pattern 2 l; Rewrite double_var.
-Ring.
-Ring.
-Intro.
-Assert H20 := (Rle_sym2 ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` r).
-Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H20 H18)). 
-Assumption.
-Rewrite <- Ropp_O; Replace ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` with ``-(l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))-(f c))/(Rmin (delta/2) ((b+ -c)/2))))``.
-Apply Rgt_Ropp; Change ``0<l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))-(f c))/(Rmin (delta/2) ((b+ -c)/2)))``; Apply gt0_plus_ge0_is_gt0; [Assumption | Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Assumption].
-Ring.
-Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption.
-Replace ``((f (c+(Rmin (delta/2) ((b-c)/2))))-(f c))/(Rmin (delta/2) ((b-c)/2))`` with ``- (((f c)-(f (c+(Rmin (delta/2) ((b-c)/2)))))/(Rmin (delta/2) ((b-c)/2)))``.
-Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Unfold Rdiv; Apply Rmult_le_pos; [Generalize (Rle_compatibility_r ``-(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` ``(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` (f c) H15); Rewrite Rplus_Ropp_r; Intro; Assumption | Left; Apply Rlt_Rinv; Assumption].
-Unfold Rdiv.
-Rewrite <- Ropp_mul1.
-Repeat Rewrite <- (Rmult_sym ``/(Rmin (delta*/2) ((b-c)*/2))``).
-Apply r_Rmult_mult with ``(Rmin (delta*/2) ((b-c)*/2))``.
-Repeat Rewrite <- Rmult_assoc.
-Rewrite <- Rinv_r_sym.
-Repeat Rewrite Rmult_1l.
-Ring.
-Red; Intro.
-Unfold Rdiv in H12; Rewrite H16 in H12; Elim (Rlt_antirefl ``0`` H12).
-Red; Intro.
-Unfold Rdiv in H12; Rewrite H16 in H12; Elim (Rlt_antirefl ``0`` H12).
-Assert H14 := (Rmin_r ``(delta/2)`` ``((b-c)/2)``).
-Assert H15 := (Rle_compatibility ``c`` ``(Rmin (delta/2) ((b-c)/2))`` ``(b-c)/2`` H14).
-Apply Rle_lt_trans with ``c+(b-c)/2``.
-Assumption.
-Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Replace ``2*(c+(b-c)/2)`` with ``c+b``.
-Replace ``2*b`` with ``b+b``.
-Apply Rlt_compatibility_r; Assumption.
-Ring.
-Unfold Rdiv; Rewrite Rmult_Rplus_distr.
-Repeat Rewrite (Rmult_sym ``2``).
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Ring.
-DiscrR.
-Apply Rlt_trans with c.
-Assumption.
-Pattern 1 c; Rewrite <- (Rplus_Or c); Apply Rlt_compatibility; Assumption.
-Cut ``0<delta/2``.
-Intro; Apply (Rmin_stable_in_posreal (mkposreal ``delta/2`` H12) (mkposreal ``(b-c)/2`` H8)).
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Sup0].
-Unfold Rabsolu; Case (case_Rabsolu (Rmin ``delta/2`` ``(b-c)/2``)).
-Intro.
-Cut ``0<delta/2``.
-Intro.
-Generalize (Rmin_stable_in_posreal (mkposreal ``delta/2`` H10) (mkposreal ``(b-c)/2`` H8)); Simpl; Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rmin (delta/2) ((b-c)/2))`` ``0`` H11 r)).
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Sup0].
-Intro; Apply Rle_lt_trans with ``delta/2``.
-Apply Rmin_l.
-Unfold Rdiv; Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l.
-Replace ``2*delta`` with ``delta+delta``. 
-Pattern 2 delta; Rewrite <- (Rplus_Or delta); Apply Rlt_compatibility.
-Rewrite Rplus_Or; Apply (cond_pos delta).
-Symmetry; Apply double.
-DiscrR.
-Cut ``0<delta/2``.
-Intro; Generalize (Rmin_stable_in_posreal (mkposreal ``delta/2`` H9) (mkposreal ``(b-c)/2`` H8)); Simpl; Intro; Red; Intro; Rewrite H11 in H10; Elim (Rlt_antirefl ``0`` H10).
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Sup0].
-Unfold Rdiv; Apply Rmult_lt_pos.
-Generalize (Rlt_compatibility_r ``-c`` c b H0); Rewrite Rplus_Ropp_r; Intro; Assumption.
-Apply Rlt_Rinv; Sup0.
-Elim H2; Intro.
-Symmetry; Assumption.
-Generalize (derivable_derive f c pr); Intro; Elim H4; Intros l H5.
-Rewrite H5 in H3; Generalize (derive_pt_eq_1 f c l pr H5); Intro; Cut ``0< -(l/2)``.
-Intro; Elim (H6 ``-(l/2)`` H7); Intros delta H9.
-Cut ``0<(c-a)/2``.
-Intro; Cut ``(Rmax (-(delta/2)) ((a-c)/2))<0``.
-Intro; Cut ``(Rmax (-(delta/2)) ((a-c)/2))<>0``.
-Intro; Cut ``(Rabsolu (Rmax (-(delta/2)) ((a-c)/2)))<delta``.
-Intro; Generalize (H9 ``(Rmax (-(delta/2)) ((a-c)/2))`` H11 H12); Intro; Cut ``a<c+(Rmax (-(delta/2)) ((a-c)/2))``.
-Cut ``c+(Rmax (-(delta/2)) ((a-c)/2))<b``.
-Intros; Generalize (H1 ``c+(Rmax (-(delta/2)) ((a-c)/2))`` H15 H14); Intro; Cut ``0<=((f (c+(Rmax (-(delta/2)) ((a-c)/2))))-(f c))/(Rmax (-(delta/2)) ((a-c)/2))``.
-Intro; Cut ``0< -l``.
-Intro; Unfold Rminus in H13; Cut ``0<((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l``.
-Intro; Cut ``(Rabsolu (((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l)) < -(l/2)``.
-Unfold Rabsolu; Case (case_Rabsolu ``((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l``).
-Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``((f (c+(Rmax ( -(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax ( -(delta/2)) ((a+ -c)/2))+ -l`` ``0`` H19 r)).
-Intros; Generalize (Rlt_compatibility_r ``l`` ``(((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2)))+ -l`` ``-(l/2)`` H20); Repeat Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Replace ``-(l/2)+l`` with ``l/2``.
-Cut ``l/2<0``.
-Intros; Generalize (Rlt_trans ``((f (c+(Rmax ( -(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax ( -(delta/2)) ((a+ -c)/2))`` ``l/2`` ``0`` H22 H21); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (c+(Rmax ( -(delta/2)) ((a-c)/2))))-(f c))/(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H17 H23)).
-Rewrite <- (Ropp_Ropp ``l/2``); Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption.
-Pattern 3 l; Rewrite double_var.
-Ring.
-Assumption.
-Apply ge0_plus_gt0_is_gt0; Assumption.
-Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption.
-Unfold Rdiv; Replace ``((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c))*/(Rmax ( -(delta*/2)) ((a-c)*/2))`` with ``(-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c)))*/(-(Rmax ( -(delta*/2)) ((a-c)*/2)))``.
-Apply Rmult_le_pos.
-Generalize (Rle_compatibility ``-(f (c+(Rmax (-(delta*/2)) ((a-c)*/2))))`` ``(f (c+(Rmax (-(delta*/2)) ((a-c)*/2))))`` (f c) H16); Rewrite Rplus_Ropp_l; Replace ``-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c))`` with ``-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2)))))+(f c)``.
-Intro; Assumption.
-Ring.
-Left; Apply Rlt_Rinv; Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption.
-Unfold Rdiv.
-Rewrite <- Ropp_Rinv.
-Rewrite Ropp_mul2.
-Reflexivity.
-Unfold Rdiv in H11; Assumption.
-Generalize (Rlt_compatibility c ``(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H10); Rewrite Rplus_Or; Intro; Apply Rlt_trans with ``c``; Assumption.
-Generalize (RmaxLess2 ``(-(delta/2))`` ``((a-c)/2)``); Intro; Generalize (Rle_compatibility c ``(a-c)/2`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` H14); Intro; Apply Rlt_le_trans with ``c+(a-c)/2``.
-Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Replace ``2*(c+(a-c)/2)`` with ``a+c``.
-Rewrite double.
-Apply Rlt_compatibility; Assumption.
-Ring.
-Rewrite <- Rplus_assoc.
-Rewrite <- double_var.
-Ring.
-Assumption.
-Unfold Rabsolu; Case (case_Rabsolu (Rmax ``-(delta/2)`` ``(a-c)/2``)).
-Intro; Generalize (RmaxLess1 ``-(delta/2)`` ``(a-c)/2``); Intro; Generalize (Rle_Ropp ``-(delta/2)`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` H12); Rewrite Ropp_Ropp; Intro; Generalize (Rle_sym2 ``-(Rmax ( -(delta/2)) ((a-c)/2))`` ``delta/2`` H13); Intro; Apply Rle_lt_trans with ``delta/2``.
-Assumption.
-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.
-Pattern 2 delta; Rewrite <- (Rplus_Or delta); Apply Rlt_compatibility; Rewrite Rplus_Or; Apply (cond_pos delta).
-DiscrR. 
-Cut ``-(delta/2) < 0``.
-Cut ``(a-c)/2<0``.
-Intros; Generalize (Rmax_stable_in_negreal (mknegreal ``-(delta/2)`` H13) (mknegreal ``(a-c)/2`` H12)); Simpl; Intro; Generalize (Rle_sym2 ``0`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` r); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H15 H14)).
-Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp ``(a-c)/2``); Apply Rlt_Ropp; Replace ``-((a-c)/2)`` with ``(c-a)/2``.
-Assumption.
-Unfold Rdiv.
-Rewrite <- Ropp_mul1. 
-Rewrite (Ropp_distr2 a c).
-Reflexivity.
-Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)]].
-Red; Intro; Rewrite H11 in H10; Elim (Rlt_antirefl ``0`` H10).
-Cut ``(a-c)/2<0``.
-Intro; Cut ``-(delta/2)<0``.
-Intro; Apply (Rmax_stable_in_negreal (mknegreal ``-(delta/2)`` H11) (mknegreal ``(a-c)/2`` H10)).
-Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)]].
-Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp ``(a-c)/2``); Apply Rlt_Ropp; Replace ``-((a-c)/2)`` with ``(c-a)/2``.
-Assumption.
-Unfold Rdiv.
-Rewrite <- Ropp_mul1. 
-Rewrite (Ropp_distr2 a c).
-Reflexivity.
-Unfold Rdiv; Apply Rmult_lt_pos; [Generalize (Rlt_compatibility_r ``-a`` a c H); Rewrite Rplus_Ropp_r; Intro; Assumption | Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)]].
-Replace ``-(l/2)`` with ``(-l)/2``.
-Unfold Rdiv; Apply Rmult_lt_pos.
-Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption.
-Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)].
-Unfold Rdiv; Apply Ropp_mul1.
-Qed.
-
-Theorem deriv_minimum : (f:R->R;a,b,c:R;pr:(derivable_pt f c)) ``a<c``->``c<b``->((x:R) ``a<x``->``x<b``->``(f c)<=(f x)``)->``(derive_pt f c pr)==0``.
-Intros.
-Rewrite <- (Ropp_Ropp (derive_pt f c pr)).
-Apply eq_RoppO.
-Rewrite <- (derive_pt_opp f c pr).
-Cut (x:R)(``a<x``->``x<b``->``((opp_fct f) x)<=((opp_fct f) c)``).
-Intro.
-Apply (deriv_maximum (opp_fct f) a b c (derivable_pt_opp ? ? pr) H H0 H2).
-Intros; Unfold opp_fct; Apply Rge_Ropp; Apply Rle_sym1.
-Apply (H1 x H2 H3).
+Theorem deriv_maximum :
+ forall f (a b c:R) (pr:derivable_pt f c),
+   a < c ->
+   c < b ->
+   (forall x:R, a < x -> x < b -> f x <= f c) -> derive_pt f c pr = 0.
+intros; case (Rtotal_order 0 (derive_pt f c pr)); intro.
+assert (H3 := derivable_derive f c pr).
+elim H3; intros l H4; rewrite H4 in H2.
+assert (H5 := derive_pt_eq_1 f c l pr H4).
+cut (0 < l / 2);
+ [ intro
+ | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
+elim (H5 (l / 2) H6); intros delta H7.
+cut (0 < (b - c) / 2).
+intro; cut (Rmin (delta / 2) ((b - c) / 2) <> 0).
+intro; cut (Rabs (Rmin (delta / 2) ((b - c) / 2)) < delta).
+intro.
+assert (H11 := H7 (Rmin (delta / 2) ((b - c) / 2)) H9 H10).
+cut (0 < Rmin (delta / 2) ((b - c) / 2)).
+intro; cut (a < c + Rmin (delta / 2) ((b - c) / 2)).
+intro; cut (c + Rmin (delta / 2) ((b - c) / 2) < b).
+intro; assert (H15 := H1 (c + Rmin (delta / 2) ((b - c) / 2)) H13 H14).
+cut
+ ((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) /
+  Rmin (delta / 2) ((b - c) / 2) <= 0).
+intro; cut (- l < 0).
+intro; unfold Rminus in H11.
+cut
+ ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+  Rmin (delta / 2) ((b + - c) / 2) + - l < 0).
+intro;
+ cut
+  (Rabs
+     ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+      Rmin (delta / 2) ((b + - c) / 2) + - l) < l / 2).
+unfold Rabs in |- *;
+ case
+  (Rcase_abs
+     ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+      Rmin (delta / 2) ((b + - c) / 2) + - l)); intro.
+replace
+ (-
+  ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+   Rmin (delta / 2) ((b + - c) / 2) + - l)) with
+ (l +
+  -
+  ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+   Rmin (delta / 2) ((b + - c) / 2))).
+intro;
+ generalize
+  (Rplus_lt_compat_l (- l)
+     (l +
+      -
+      ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+       Rmin (delta / 2) ((b + - c) / 2))) (l / 2) H19);
+ repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; 
+ rewrite Rplus_0_l; replace (- l + l / 2) with (- (l / 2)).
+intro;
+ generalize
+  (Ropp_lt_gt_contravar
+     (-
+      ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+       Rmin (delta / 2) ((b + - c) / 2))) (- (l / 2)) H20);
+ repeat rewrite Ropp_involutive; intro;
+ generalize
+  (Rlt_trans 0 (l / 2)
+     ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+      Rmin (delta / 2) ((b + - c) / 2)) H6 H21); intro;
+ elim
+  (Rlt_irrefl 0
+     (Rlt_le_trans 0
+        ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+         Rmin (delta / 2) ((b + - c) / 2)) 0 H22 H16)).
+pattern l at 2 in |- *; rewrite double_var.
+ring.
+ring.
+intro.
+assert
+ (H20 :=
+  Rge_le
+    ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+     Rmin (delta / 2) ((b + - c) / 2) + - l) 0 r).
+elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H20 H18)). 
+assumption.
+rewrite <- Ropp_0;
+ replace
+  ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) /
+   Rmin (delta / 2) ((b + - c) / 2) + - l) with
+  (-
+   (l +
+    -
+    ((f (c + Rmin (delta / 2) ((b + - c) / 2)) - f c) /
+     Rmin (delta / 2) ((b + - c) / 2)))).
+apply Ropp_gt_lt_contravar;
+ change
+   (0 <
+    l +
+    -
+    ((f (c + Rmin (delta / 2) ((b + - c) / 2)) - f c) /
+     Rmin (delta / 2) ((b + - c) / 2))) in |- *; apply Rplus_lt_le_0_compat;
+ [ assumption
+ | rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption ].
+ring.
+rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
+replace
+ ((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) /
+  Rmin (delta / 2) ((b - c) / 2)) with
+ (-
+  ((f c - f (c + Rmin (delta / 2) ((b - c) / 2))) /
+   Rmin (delta / 2) ((b - c) / 2))).
+rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge;
+ unfold Rdiv in |- *; apply Rmult_le_pos;
+ [ generalize
+    (Rplus_le_compat_r (- f (c + Rmin (delta * / 2) ((b - c) * / 2)))
+       (f (c + Rmin (delta * / 2) ((b - c) * / 2))) (
+       f c) H15); rewrite Rplus_opp_r; intro; assumption
+ | left; apply Rinv_0_lt_compat; assumption ].
+unfold Rdiv in |- *.
+rewrite <- Ropp_mult_distr_l_reverse.
+repeat rewrite <- (Rmult_comm (/ Rmin (delta * / 2) ((b - c) * / 2))).
+apply Rmult_eq_reg_l with (Rmin (delta * / 2) ((b - c) * / 2)).
+repeat rewrite <- Rmult_assoc.
+rewrite <- Rinv_r_sym.
+repeat rewrite Rmult_1_l.
+ring.
+red in |- *; intro.
+unfold Rdiv in H12; rewrite H16 in H12; elim (Rlt_irrefl 0 H12).
+red in |- *; intro.
+unfold Rdiv in H12; rewrite H16 in H12; elim (Rlt_irrefl 0 H12).
+assert (H14 := Rmin_r (delta / 2) ((b - c) / 2)).
+assert
+ (H15 :=
+  Rplus_le_compat_l c (Rmin (delta / 2) ((b - c) / 2)) ((b - c) / 2) H14).
+apply Rle_lt_trans with (c + (b - c) / 2).
+assumption.
+apply Rmult_lt_reg_l with 2.
+prove_sup0.
+replace (2 * (c + (b - c) / 2)) with (c + b).
+replace (2 * b) with (b + b).
+apply Rplus_lt_compat_r; assumption.
+ring.
+unfold Rdiv in |- *; rewrite Rmult_plus_distr_l.
+repeat rewrite (Rmult_comm 2).
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_r.
+ring.
+discrR.
+apply Rlt_trans with c.
+assumption.
+pattern c at 1 in |- *; rewrite <- (Rplus_0_r c); apply Rplus_lt_compat_l;
+ assumption.
+cut (0 < delta / 2).
+intro;
+ apply
+  (Rmin_stable_in_posreal (mkposreal (delta / 2) H12)
+     (mkposreal ((b - c) / 2) H8)).
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
+unfold Rabs in |- *; case (Rcase_abs (Rmin (delta / 2) ((b - c) / 2))).
+intro.
+cut (0 < delta / 2).
+intro.
+generalize
+ (Rmin_stable_in_posreal (mkposreal (delta / 2) H10)
+    (mkposreal ((b - c) / 2) H8)); simpl in |- *; intro;
+ elim (Rlt_irrefl 0 (Rlt_trans 0 (Rmin (delta / 2) ((b - c) / 2)) 0 H11 r)).
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
+intro; apply Rle_lt_trans with (delta / 2).
+apply Rmin_l.
+unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2.
+prove_sup0.
+rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
+rewrite Rmult_1_l.
+replace (2 * delta) with (delta + delta). 
+pattern delta at 2 in |- *; rewrite <- (Rplus_0_r delta);
+ apply Rplus_lt_compat_l.
+rewrite Rplus_0_r; apply (cond_pos delta).
+symmetry  in |- *; apply double.
+discrR.
+cut (0 < delta / 2).
+intro;
+ generalize
+  (Rmin_stable_in_posreal (mkposreal (delta / 2) H9)
+     (mkposreal ((b - c) / 2) H8)); simpl in |- *; 
+ intro; red in |- *; intro; rewrite H11 in H10; elim (Rlt_irrefl 0 H10).
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
+unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+generalize (Rplus_lt_compat_r (- c) c b H0); rewrite Rplus_opp_r; intro;
+ assumption.
+apply Rinv_0_lt_compat; prove_sup0.
+elim H2; intro.
+symmetry  in |- *; assumption.
+generalize (derivable_derive f c pr); intro; elim H4; intros l H5.
+rewrite H5 in H3; generalize (derive_pt_eq_1 f c l pr H5); intro;
+ cut (0 < - (l / 2)).
+intro; elim (H6 (- (l / 2)) H7); intros delta H9.
+cut (0 < (c - a) / 2).
+intro; cut (Rmax (- (delta / 2)) ((a - c) / 2) < 0).
+intro; cut (Rmax (- (delta / 2)) ((a - c) / 2) <> 0).
+intro; cut (Rabs (Rmax (- (delta / 2)) ((a - c) / 2)) < delta).
+intro; generalize (H9 (Rmax (- (delta / 2)) ((a - c) / 2)) H11 H12); intro;
+ cut (a < c + Rmax (- (delta / 2)) ((a - c) / 2)).
+cut (c + Rmax (- (delta / 2)) ((a - c) / 2) < b).
+intros; generalize (H1 (c + Rmax (- (delta / 2)) ((a - c) / 2)) H15 H14);
+ intro;
+ cut
+  (0 <=
+   (f (c + Rmax (- (delta / 2)) ((a - c) / 2)) - f c) /
+   Rmax (- (delta / 2)) ((a - c) / 2)).
+intro; cut (0 < - l).
+intro; unfold Rminus in H13;
+ cut
+  (0 <
+   (f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
+   Rmax (- (delta / 2)) ((a + - c) / 2) + - l).
+intro;
+ cut
+  (Rabs
+     ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
+      Rmax (- (delta / 2)) ((a + - c) / 2) + - l) < 
+   - (l / 2)).
+unfold Rabs in |- *;
+ case
+  (Rcase_abs
+     ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
+      Rmax (- (delta / 2)) ((a + - c) / 2) + - l)).
+intro;
+ elim
+  (Rlt_irrefl 0
+     (Rlt_trans 0
+        ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
+         Rmax (- (delta / 2)) ((a + - c) / 2) + - l) 0 H19 r)).
+intros;
+ generalize
+  (Rplus_lt_compat_r l
+     ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
+      Rmax (- (delta / 2)) ((a + - c) / 2) + - l) (
+     - (l / 2)) H20); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l;
+ rewrite Rplus_0_r; replace (- (l / 2) + l) with (l / 2).
+cut (l / 2 < 0).
+intros;
+ generalize
+  (Rlt_trans
+     ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) /
+      Rmax (- (delta / 2)) ((a + - c) / 2)) (l / 2) 0 H22 H21); 
+ intro;
+ elim
+  (Rlt_irrefl 0
+     (Rle_lt_trans 0
+        ((f (c + Rmax (- (delta / 2)) ((a - c) / 2)) - f c) /
+         Rmax (- (delta / 2)) ((a - c) / 2)) 0 H17 H23)).
+rewrite <- (Ropp_involutive (l / 2)); rewrite <- Ropp_0;
+ apply Ropp_lt_gt_contravar; assumption.
+pattern l at 3 in |- *; rewrite double_var.
+ring.
+assumption.
+apply Rplus_le_lt_0_compat; assumption.
+rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
+unfold Rdiv in |- *;
+ replace
+  ((f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c) *
+   / Rmax (- (delta * / 2)) ((a - c) * / 2)) with
+  (- (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c) *
+   / - Rmax (- (delta * / 2)) ((a - c) * / 2)).
+apply Rmult_le_pos.
+generalize
+ (Rplus_le_compat_l (- f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)))
+    (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2))) (
+    f c) H16); rewrite Rplus_opp_l;
+ replace (- (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c)) with
+  (- f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) + f c).
+intro; assumption.
+ring.
+left; apply Rinv_0_lt_compat; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar;
+ assumption.
+unfold Rdiv in |- *.
+rewrite <- Ropp_inv_permute.
+rewrite Rmult_opp_opp.
+reflexivity.
+unfold Rdiv in H11; assumption.
+generalize (Rplus_lt_compat_l c (Rmax (- (delta / 2)) ((a - c) / 2)) 0 H10);
+ rewrite Rplus_0_r; intro; apply Rlt_trans with c; 
+ assumption.
+generalize (RmaxLess2 (- (delta / 2)) ((a - c) / 2)); intro;
+ generalize
+  (Rplus_le_compat_l c ((a - c) / 2) (Rmax (- (delta / 2)) ((a - c) / 2)) H14);
+ intro; apply Rlt_le_trans with (c + (a - c) / 2).
+apply Rmult_lt_reg_l with 2.
+prove_sup0.
+replace (2 * (c + (a - c) / 2)) with (a + c).
+rewrite double.
+apply Rplus_lt_compat_l; assumption.
+ring.
+rewrite <- Rplus_assoc.
+rewrite <- double_var.
+ring.
+assumption.
+unfold Rabs in |- *; case (Rcase_abs (Rmax (- (delta / 2)) ((a - c) / 2))).
+intro; generalize (RmaxLess1 (- (delta / 2)) ((a - c) / 2)); intro;
+ generalize
+  (Ropp_le_ge_contravar (- (delta / 2)) (Rmax (- (delta / 2)) ((a - c) / 2))
+     H12); rewrite Ropp_involutive; intro;
+ generalize (Rge_le (delta / 2) (- Rmax (- (delta / 2)) ((a - c) / 2)) H13);
+ intro; apply Rle_lt_trans with (delta / 2).
+assumption.
+apply Rmult_lt_reg_l with 2. 
+prove_sup0.
+unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
+ rewrite <- Rinv_r_sym.
+rewrite Rmult_1_l; rewrite double.
+pattern delta at 2 in |- *; rewrite <- (Rplus_0_r delta);
+ apply Rplus_lt_compat_l; rewrite Rplus_0_r; apply (cond_pos delta).
+discrR. 
+cut (- (delta / 2) < 0).
+cut ((a - c) / 2 < 0).
+intros;
+ generalize
+  (Rmax_stable_in_negreal (mknegreal (- (delta / 2)) H13)
+     (mknegreal ((a - c) / 2) H12)); simpl in |- *; 
+ intro; generalize (Rge_le (Rmax (- (delta / 2)) ((a - c) / 2)) 0 r); 
+ intro;
+ elim
+  (Rlt_irrefl 0
+     (Rle_lt_trans 0 (Rmax (- (delta / 2)) ((a - c) / 2)) 0 H15 H14)).
+rewrite <- Ropp_0; rewrite <- (Ropp_involutive ((a - c) / 2));
+ apply Ropp_lt_gt_contravar; replace (- ((a - c) / 2)) with ((c - a) / 2).
+assumption.
+unfold Rdiv in |- *.
+rewrite <- Ropp_mult_distr_l_reverse. 
+rewrite (Ropp_minus_distr a c).
+reflexivity.
+rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; unfold Rdiv in |- *;
+ apply Rmult_lt_0_compat;
+ [ apply (cond_pos delta)
+ | assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ].
+red in |- *; intro; rewrite H11 in H10; elim (Rlt_irrefl 0 H10).
+cut ((a - c) / 2 < 0).
+intro; cut (- (delta / 2) < 0).
+intro;
+ apply
+  (Rmax_stable_in_negreal (mknegreal (- (delta / 2)) H11)
+     (mknegreal ((a - c) / 2) H10)).
+rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; unfold Rdiv in |- *;
+ apply Rmult_lt_0_compat;
+ [ apply (cond_pos delta)
+ | assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ].
+rewrite <- Ropp_0; rewrite <- (Ropp_involutive ((a - c) / 2));
+ apply Ropp_lt_gt_contravar; replace (- ((a - c) / 2)) with ((c - a) / 2).
+assumption.
+unfold Rdiv in |- *.
+rewrite <- Ropp_mult_distr_l_reverse. 
+rewrite (Ropp_minus_distr a c).
+reflexivity.
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ generalize (Rplus_lt_compat_r (- a) a c H); rewrite Rplus_opp_r; intro;
+    assumption
+ | assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ].
+replace (- (l / 2)) with (- l / 2).
+unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
+assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ].
+unfold Rdiv in |- *; apply Ropp_mult_distr_l_reverse.
+Qed.
+
+Theorem deriv_minimum :
+ forall f (a b c:R) (pr:derivable_pt f c),
+   a < c ->
+   c < b ->
+   (forall x:R, a < x -> x < b -> f c <= f x) -> derive_pt f c pr = 0.
+intros.
+rewrite <- (Ropp_involutive (derive_pt f c pr)).
+apply Ropp_eq_0_compat.
+rewrite <- (derive_pt_opp f c pr).
+cut (forall x:R, a < x -> x < b -> (- f)%F x <= (- f)%F c).
+intro.
+apply (deriv_maximum (- f)%F a b c (derivable_pt_opp _ _ pr) H H0 H2).
+intros; unfold opp_fct in |- *; apply Ropp_ge_le_contravar; apply Rle_ge.
+apply (H1 x H2 H3).
 Qed.
  
-Theorem deriv_constant2 : (f:R->R;a,b,c:R;pr:(derivable_pt f c)) ``a<c``->``c<b``->((x:R) ``a<x``->``x<b``->``(f x)==(f c)``)->``(derive_pt f c pr)==0``.
-Intros.
-EApply deriv_maximum with a b; Try Assumption.
-Intros; Right; Apply (H1 x H2 H3).
+Theorem deriv_constant2 :
+ forall f (a b c:R) (pr:derivable_pt f c),
+   a < c ->
+   c < b -> (forall x:R, a < x -> x < b -> f x = f c) -> derive_pt f c pr = 0.
+intros.
+eapply deriv_maximum with a b; try assumption.
+intros; right; apply (H1 x H2 H3).
 Qed.
 
 (**********)
-Lemma nonneg_derivative_0 : (f:R->R;pr:(derivable f)) (increasing f) -> ((x:R) ``0<=(derive_pt f x (pr x))``).
-Intros; Unfold increasing in H.
-Assert H0 := (derivable_derive f x (pr x)).
-Elim H0; Intros l H1.
-Rewrite H1; Case (total_order R0 l); Intro.
-Left; Assumption.
-Elim H2; Intro.
-Right; Assumption.
-Assert H4 := (derive_pt_eq_1 f x l (pr x) H1).
-Cut ``0< -(l/2)``.
-Intro; Elim (H4 ``-(l/2)`` H5); Intros delta H6.
-Cut ``delta/2<>0``/\``0<delta/2``/\``(Rabsolu delta/2)<delta``.
-Intro; Decompose [and] H7; Intros; Generalize (H6 ``delta/2`` H8 H11); Cut ``0<=((f (x+delta/2))-(f x))/(delta/2)``.
-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``).
-Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` H12 r)).
-Intros; Generalize (Rlt_compatibility_r l ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``-(l/2)`` H13); Unfold Rminus; Replace ``-(l/2)+l`` with ``l/2``.
-Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Intro; Generalize (Rle_lt_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``l/2`` H9 H14); Intro; Cut ``l/2<0``.
-Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``l/2`` ``0`` H15 H16)).
-Rewrite <- Ropp_O in H5; Generalize (Rlt_Ropp ``-0`` ``-(l/2)`` H5); Repeat Rewrite Ropp_Ropp; Intro; Assumption.
-Pattern 3 l ; Rewrite double_var.
-Ring.
-Unfold Rminus; Apply ge0_plus_ge0_is_ge0.
-Unfold Rdiv; Apply Rmult_le_pos.
-Cut ``x<=(x+(delta*/2))``.
-Intro; Generalize (H x ``x+(delta*/2)`` H12); Intro; Generalize (Rle_compatibility ``-(f x)`` ``(f x)`` ``(f (x+delta*/2))`` 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.
-Left; Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption.
-Unfold Rdiv; Apply Rmult_le_pos.
-Cut ``x<=(x+(delta*/2))``.
-Intro; Generalize (H x ``x+(delta*/2)`` H9); Intro; Generalize (Rle_compatibility ``-(f x)`` ``(f x)`` ``(f (x+delta*/2))`` H12); 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.
-Split.
-Unfold Rdiv; Apply prod_neq_R0.
-Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H7; Elim (Rlt_antirefl ``0`` H7).
-Apply Rinv_neq_R0; DiscrR.
-Split.
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Sup0].
-Replace ``(Rabsolu delta/2)`` with ``delta/2``.
-Unfold Rdiv; Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Rewrite (Rmult_sym ``2``).
-Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1r.
-Rewrite double.
-Pattern 1 (pos delta); Rewrite <- Rplus_Or.
-Apply Rlt_compatibility; Apply (cond_pos delta).
-Symmetry; Apply Rabsolu_right.
-Left; Change ``0<delta/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Sup0].
-Unfold Rdiv; Rewrite <- Ropp_mul1; Apply Rmult_lt_pos.
-Apply Rlt_anti_compatibility with l.
-Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Assumption.
-Apply Rlt_Rinv; Sup0.
-Qed.
+Lemma nonneg_derivative_0 :
+ forall f (pr:derivable f),
+   increasing f -> forall x:R, 0 <= derive_pt f x (pr x).
+intros; unfold increasing in H.
+assert (H0 := derivable_derive f x (pr x)).
+elim H0; intros l H1.
+rewrite H1; case (Rtotal_order 0 l); intro.
+left; assumption.
+elim H2; intro.
+right; assumption.
+assert (H4 := derive_pt_eq_1 f x l (pr x) H1).
+cut (0 < - (l / 2)).
+intro; elim (H4 (- (l / 2)) H5); intros delta H6.
+cut (delta / 2 <> 0 /\ 0 < delta / 2 /\ Rabs (delta / 2) < delta).
+intro; decompose [and] H7; intros; generalize (H6 (delta / 2) H8 H11);
+ cut (0 <= (f (x + delta / 2) - f x) / (delta / 2)).
+intro; cut (0 <= (f (x + delta / 2) - f x) / (delta / 2) - l).
+intro; unfold Rabs in |- *;
+ case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)).
+intro;
+ elim
+  (Rlt_irrefl 0
+     (Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 H12 r)).
+intros;
+ generalize
+  (Rplus_lt_compat_r l ((f (x + delta / 2) - f x) / (delta / 2) - l)
+     (- (l / 2)) H13); unfold Rminus in |- *;
+ replace (- (l / 2) + l) with (l / 2).
+rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro;
+ generalize
+  (Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2)) (l / 2) H9 H14);
+ intro; cut (l / 2 < 0).
+intro; elim (Rlt_irrefl 0 (Rlt_trans 0 (l / 2) 0 H15 H16)).
+rewrite <- Ropp_0 in H5;
+ generalize (Ropp_lt_gt_contravar (-0) (- (l / 2)) H5);
+ repeat rewrite Ropp_involutive; intro; assumption.
+pattern l at 3 in |- *; rewrite double_var.
+ring.
+unfold Rminus in |- *; apply Rplus_le_le_0_compat.
+unfold Rdiv in |- *; apply Rmult_le_pos.
+cut (x <= x + delta * / 2).
+intro; generalize (H x (x + delta * / 2) H12); intro;
+ generalize (Rplus_le_compat_l (- f x) (f x) (f (x + delta * / 2)) H13);
+ rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption.
+pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+ left; assumption.
+left; apply Rinv_0_lt_compat; assumption.
+left; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
+unfold Rdiv in |- *; apply Rmult_le_pos.
+cut (x <= x + delta * / 2).
+intro; generalize (H x (x + delta * / 2) H9); intro;
+ generalize (Rplus_le_compat_l (- f x) (f x) (f (x + delta * / 2)) H12);
+ rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption.
+pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+ left; assumption. 
+left; apply Rinv_0_lt_compat; assumption.
+split.
+unfold Rdiv in |- *; apply prod_neq_R0.
+generalize (cond_pos delta); intro; red in |- *; intro H9; rewrite H9 in H7;
+ elim (Rlt_irrefl 0 H7).
+apply Rinv_neq_0_compat; discrR.
+split.
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
+replace (Rabs (delta / 2)) with (delta / 2).
+unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2.
+prove_sup0.
+rewrite (Rmult_comm 2).
+rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
+rewrite Rmult_1_r.
+rewrite double.
+pattern (pos delta) at 1 in |- *; rewrite <- Rplus_0_r.
+apply Rplus_lt_compat_l; apply (cond_pos delta).
+symmetry  in |- *; apply Rabs_right.
+left; change (0 < delta / 2) in |- *; unfold Rdiv in |- *;
+ apply Rmult_lt_0_compat;
+ [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
+unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse;
+ apply Rmult_lt_0_compat.
+apply Rplus_lt_reg_r with l.
+unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r; assumption.
+apply Rinv_0_lt_compat; prove_sup0.
+Qed.
\ No newline at end of file