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, 375 insertions, 397 deletions

diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 4f7420306..3f56ccdf1 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -13,441 +13,419 @@
 (*                                                       *)
 (*********************************************************)
 
-Require Rbase.
-Require Rfunctions.
-Require Rlimit.
-Require Fourier.
-Require Classical_Prop.
-Require Classical_Pred_Type.
-Require Omega.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rlimit.
+Require Import Fourier.
+Require Import Classical_Prop.
+Require Import Classical_Pred_Type.
+Require Import Omega. Open Local Scope R_scope.
 
 (*********)
-Definition D_x:(R->Prop)->R->R->Prop:=[D:R->Prop][y:R][x:R]
-       (D x)/\(~y==x).
+Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x.
 
 (*********)
-Definition continue_in:(R->R)->(R->Prop)->R->Prop:=
-       [f:R->R; D:R->Prop; x0:R](limit1_in f (D_x D x0) (f x0) x0).
+Definition continue_in (f:R -> R) (D:R -> Prop) (x0:R) : Prop :=
+  limit1_in f (D_x D x0) (f x0) x0.
 
 (*********)
-Definition D_in:(R->R)->(R->R)->(R->Prop)->R->Prop:=
-  [f:R->R; d:R->R; D:R->Prop; x0:R](limit1_in 
-    [x:R] (Rdiv (Rminus (f x) (f x0)) (Rminus x x0)) 
-    (D_x D x0) (d x0) x0).
+Definition D_in (f d:R -> R) (D:R -> Prop) (x0:R) : Prop :=
+  limit1_in (fun x:R => (f x - f x0) / (x - x0)) (D_x D x0) (d x0) x0.
 
 (*********)
-Lemma cont_deriv:(f,d:R->R;D:R->Prop;x0:R)
-         (D_in f d D x0)->(continue_in f D x0).
-Unfold continue_in;Unfold D_in;Unfold limit1_in;Unfold limit_in;
- Unfold Rdiv;Simpl;Intros;Elim (H eps H0); Clear H;Intros;
- Elim H;Clear H;Intros; Elim (Req_EM (d x0) R0);Intro.
-Split with (Rmin R1 x);Split.
-Elim (Rmin_Rgt R1 x R0);Intros a b;
- Apply (b (conj (Rgt R1 R0) (Rgt x R0) Rlt_R0_R1 H)).
-Intros;Elim H3;Clear H3;Intros;
-Generalize (let (H1,H2)=(Rmin_Rgt R1 x (R_dist x1 x0)) in H1);
- Unfold Rgt;Intro;Elim (H5 H4);Clear H5;Intros;
- Generalize (H1 x1 (conj (D_x D x0 x1) (Rlt (R_dist x1 x0) x) H3 H6));
- Clear H1;Intro;Unfold D_x in H3;Elim H3;Intros.
-Rewrite H2 in H1;Unfold R_dist; Unfold R_dist in H1;
- Cut (Rlt (Rabsolu (Rminus (f x1) (f x0))) 
-          (Rmult eps (Rabsolu (Rminus x1 x0)))).
-Intro;Unfold R_dist in H5;
-  Generalize (Rlt_monotony eps ``(Rabsolu (x1-x0))`` ``1`` H0 H5);
-Rewrite Rmult_1r;Intro;Apply Rlt_trans with r2:=``eps*(Rabsolu (x1-x0))``;
- Assumption.
-Rewrite (minus_R0 ``((f x1)-(f x0))*/(x1-x0)``) in H1;
- Rewrite Rabsolu_mult in H1; Cut ``x1-x0 <> 0``.
-Intro;Rewrite (Rabsolu_Rinv (Rminus x1 x0) H9) in H1;
- Generalize (Rlt_monotony ``(Rabsolu (x1-x0))`` 
- ``(Rabsolu ((f x1)-(f x0)))*/(Rabsolu (x1-x0))`` eps 
- (Rabsolu_pos_lt ``x1-x0`` H9) H1);Intro; Rewrite Rmult_sym in H10;
- Rewrite Rmult_assoc in H10;Rewrite Rinv_l in H10.
-Rewrite Rmult_1r in H10;Rewrite Rmult_sym;Assumption.
-Apply Rabsolu_no_R0;Auto.
-Apply Rminus_eq_contra;Auto.
+Lemma cont_deriv :
+ forall (f d:R -> R) (D:R -> Prop) (x0:R),
+   D_in f d D x0 -> continue_in f D x0.
+unfold continue_in in |- *; unfold D_in in |- *; unfold limit1_in in |- *;
+ unfold limit_in in |- *; unfold Rdiv in |- *; simpl in |- *; 
+ intros; elim (H eps H0); clear H; intros; elim H; 
+ clear H; intros; elim (Req_dec (d x0) 0); intro.
+split with (Rmin 1 x); split.
+elim (Rmin_Rgt 1 x 0); intros a b; apply (b (conj Rlt_0_1 H)).
+intros; elim H3; clear H3; intros;
+ generalize (let (H1, H2) := Rmin_Rgt 1 x (R_dist x1 x0) in H1);
+ unfold Rgt in |- *; intro; elim (H5 H4); clear H5; 
+ intros; generalize (H1 x1 (conj H3 H6)); clear H1; 
+ intro; unfold D_x in H3; elim H3; intros.
+rewrite H2 in H1; unfold R_dist in |- *; unfold R_dist in H1;
+ cut (Rabs (f x1 - f x0) < eps * Rabs (x1 - x0)).
+intro; unfold R_dist in H5;
+ generalize (Rmult_lt_compat_l eps (Rabs (x1 - x0)) 1 H0 H5);
+ rewrite Rmult_1_r; intro; apply Rlt_trans with (r2 := eps * Rabs (x1 - x0));
+ assumption.
+rewrite (Rminus_0_r ((f x1 - f x0) * / (x1 - x0))) in H1;
+ rewrite Rabs_mult in H1; cut (x1 - x0 <> 0).
+intro; rewrite (Rabs_Rinv (x1 - x0) H9) in H1;
+ generalize
+  (Rmult_lt_compat_l (Rabs (x1 - x0)) (Rabs (f x1 - f x0) * / Rabs (x1 - x0))
+     eps (Rabs_pos_lt (x1 - x0) H9) H1); intro; rewrite Rmult_comm in H10;
+ rewrite Rmult_assoc in H10; rewrite Rinv_l in H10.
+rewrite Rmult_1_r in H10; rewrite Rmult_comm; assumption.
+apply Rabs_no_R0; auto.
+apply Rminus_eq_contra; auto.
 (**)
- Split with (Rmin (Rmin (Rinv (Rplus R1 R1)) x) 
-              (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))));
- Split.
-Cut (Rgt (Rmin (Rinv (Rplus R1 R1)) x) R0).
-Cut (Rgt (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) R0).
-Intros;Elim (Rmin_Rgt (Rmin (Rinv (Rplus R1 R1)) x) 
-            (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) R0);
- Intros a b;
- Apply (b (conj (Rgt (Rmin (Rinv (Rplus R1 R1)) x) R0)
-       (Rgt (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) R0)
-        H4 H3)).
-Apply Rmult_gt;Auto.
-Unfold Rgt;Apply Rlt_Rinv;Apply Rabsolu_pos_lt;Apply mult_non_zero;
- Split.
-DiscrR.
-Assumption.
-Elim (Rmin_Rgt (Rinv (Rplus R1 R1)) x R0);Intros a b;
- Cut (Rlt R0 (Rplus R1 R1)).
-Intro;Generalize (Rlt_Rinv (Rplus R1 R1) H3);Intro;
- Fold (Rgt (Rinv (Rplus R1 R1)) R0) in H4;
- Apply (b (conj (Rgt (Rinv (Rplus R1 R1)) R0) (Rgt x R0) H4 H)).
-Fourier.
-Intros;Elim H3;Clear H3;Intros;
- Generalize (let (H1,H2)=(Rmin_Rgt (Rmin (Rinv (Rplus R1 R1)) x)
-       (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0)))))
-       (R_dist x1 x0)) in H1);Unfold Rgt;Intro;Elim (H5 H4);Clear H5;
- Intros;
- Generalize (let (H1,H2)=(Rmin_Rgt (Rinv (Rplus R1 R1)) x
-          (R_dist x1 x0)) in H1);Unfold Rgt;Intro;Elim (H7 H5);Clear H7;
- Intros;Clear H4 H5;
- Generalize (H1 x1 (conj (D_x D x0 x1) (Rlt (R_dist x1 x0) x) H3 H8));
- Clear H1;Intro;Unfold D_x in H3;Elim H3;Intros;
- Generalize (sym_not_eqT R x0 x1 H5);Clear H5;Intro H5;
- Generalize (Rminus_eq_contra x1 x0 H5);
- Intro;Generalize H1;Pattern 1 (d x0); 
- Rewrite <-(let (H1,H2)=(Rmult_ne (d x0)) in H2);
- Rewrite <-(Rinv_l (Rminus x1 x0) H9); Unfold R_dist;Unfold 1 Rminus;
- Rewrite (Rmult_sym (Rminus (f x1) (f x0)) (Rinv (Rminus x1 x0)));
- Rewrite (Rmult_sym (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)) (d x0));
- Rewrite <-(Ropp_mul1 (d x0) (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)));
- Rewrite (Rmult_sym (Ropp (d x0))
-                    (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)));
- Rewrite (Rmult_assoc (Rinv (Rminus x1 x0)) (Rminus x1 x0) (Ropp (d x0)));
- Rewrite <-(Rmult_Rplus_distr (Rinv (Rminus x1 x0)) (Rminus (f x1) (f x0))
-                   (Rmult (Rminus x1 x0) (Ropp (d x0))));
- Rewrite (Rabsolu_mult (Rinv (Rminus x1 x0))
-                       (Rplus (Rminus (f x1) (f x0))
-                              (Rmult (Rminus x1 x0) (Ropp (d x0)))));
- Clear H1;Intro;Generalize (Rlt_monotony (Rabsolu (Rminus x1 x0)) 
-        (Rmult (Rabsolu (Rinv (Rminus x1 x0)))
-           (Rabsolu
-             (Rplus (Rminus (f x1) (f x0))
-               (Rmult (Rminus x1 x0) (Ropp (d x0)))))) eps 
-        (Rabsolu_pos_lt (Rminus x1 x0) H9) H1); 
- Rewrite <-(Rmult_assoc (Rabsolu (Rminus x1 x0)) 
-                 (Rabsolu (Rinv (Rminus x1 x0)))
-               (Rabsolu
-           (Rplus (Rminus (f x1) (f x0))
-             (Rmult (Rminus x1 x0) (Ropp (d x0)))))); 
- Rewrite (Rabsolu_Rinv (Rminus x1 x0) H9);
- Rewrite (Rinv_r (Rabsolu (Rminus x1 x0)) 
-                 (Rabsolu_no_R0 (Rminus x1 x0) H9));
- Rewrite (let (H1,H2)=(Rmult_ne (Rabsolu
-         (Rplus (Rminus (f x1) (f x0))
-           (Rmult (Rminus x1 x0) (Ropp (d x0)))))) in H2);
- Generalize (Rabsolu_triang_inv (Rminus (f x1) (f x0))
-         (Rmult (Rminus x1 x0) (d x0)));Intro;
- Rewrite (Rmult_sym (Rminus x1 x0) (Ropp (d x0)));
- Rewrite (Ropp_mul1 (d x0) (Rminus x1 x0));
- Fold (Rminus (Rminus (f x1) (f x0)) (Rmult (d x0) (Rminus x1 x0)));
- Rewrite (Rmult_sym (Rminus x1 x0) (d x0)) in H10;
- Clear H1;Intro;Generalize (Rle_lt_trans 
-           (Rminus (Rabsolu (Rminus (f x1) (f x0)))
-           (Rabsolu (Rmult (d x0) (Rminus x1 x0))))
-          (Rabsolu
-           (Rminus (Rminus (f x1) (f x0)) (Rmult (d x0) (Rminus x1 x0))))
-          (Rmult (Rabsolu (Rminus x1 x0)) eps) H10 H1);
- Clear H1;Intro;
- Generalize (Rlt_compatibility (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
-   (Rminus (Rabsolu (Rminus (f x1) (f x0)))
-           (Rabsolu (Rmult (d x0) (Rminus x1 x0))))
-   (Rmult (Rabsolu (Rminus x1 x0)) eps) H1);
- Unfold 2 Rminus;Rewrite (Rplus_sym (Rabsolu (Rminus (f x1) (f x0)))
-    (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0)))));
- Rewrite <-(Rplus_assoc (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
-  (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0)))) 
-  (Rabsolu (Rminus (f x1) (f x0))));
- Rewrite (Rplus_Ropp_r (Rabsolu (Rmult (d x0) (Rminus x1 x0))));
- Rewrite (let (H1,H2)=(Rplus_ne (Rabsolu (Rminus (f x1) (f x0)))) in H2);
- Clear H1;Intro;Cut (Rlt (Rplus (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
-           (Rmult (Rabsolu (Rminus x1 x0)) eps)) eps).
-Intro;Apply (Rlt_trans (Rabsolu (Rminus (f x1) (f x0))) 
-    (Rplus (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
-            (Rmult (Rabsolu (Rminus x1 x0)) eps)) eps H1 H11). 
-Clear H1 H5 H3 H10;Generalize (Rabsolu_pos_lt (d x0) H2);
- Intro;Unfold Rgt in H0;Generalize (Rlt_monotony eps (R_dist x1 x0)
-       (Rinv (Rplus R1 R1)) H0 H7);Clear H7;Intro;
- Generalize (Rlt_monotony (Rabsolu (d x0)) (R_dist x1 x0) 
-    (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) H1 H6);
- Clear H6;Intro;Rewrite (Rmult_sym eps (R_dist x1 x0)) in H3; 
- Unfold R_dist in H3 H5;
- Rewrite <-(Rabsolu_mult (d x0) (Rminus x1 x0)) in H5;
- Rewrite (Rabsolu_mult (Rplus R1 R1) (d x0)) in H5;
- Cut ~(Rabsolu (Rplus R1 R1))==R0.
-Intro;Fold (Rgt (Rabsolu (d x0)) R0) in H1;
- Rewrite (Rinv_Rmult (Rabsolu (Rplus R1 R1)) (Rabsolu (d x0))
- H6 (imp_not_Req (Rabsolu (d x0)) R0 
-  (or_intror (Rlt (Rabsolu (d x0)) R0) (Rgt (Rabsolu (d x0)) R0) H1))) 
-  in H5;
- Rewrite (Rmult_sym (Rabsolu (d x0)) (Rmult eps
-             (Rmult (Rinv (Rabsolu (Rplus R1 R1)))
-               (Rinv (Rabsolu (d x0)))))) in H5;
- Rewrite <-(Rmult_assoc eps (Rinv (Rabsolu (Rplus R1 R1))) 
-   (Rinv (Rabsolu (d x0)))) in H5;
- Rewrite (Rmult_assoc (Rmult eps (Rinv (Rabsolu (Rplus R1 R1))))
-    (Rinv (Rabsolu (d x0))) (Rabsolu (d x0))) in H5;
- Rewrite (Rinv_l (Rabsolu (d x0)) (imp_not_Req (Rabsolu (d x0)) R0 
-  (or_intror (Rlt (Rabsolu (d x0)) R0) (Rgt (Rabsolu (d x0)) R0) H1))) 
-  in H5;
- Rewrite (let (H1,H2)=(Rmult_ne (Rmult eps (Rinv (Rabsolu (Rplus R1 R1)))))
-   in H1) in H5;Cut (Rabsolu (Rplus R1 R1))==(Rplus R1 R1).
-Intro;Rewrite H7 in H5;
- Generalize (Rplus_lt (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
-        (Rmult eps (Rinv (Rplus R1 R1)))
-        (Rmult (Rabsolu (Rminus x1 x0)) eps)
-        (Rmult eps (Rinv (Rplus R1 R1))) H5 H3);Intro;
- Rewrite eps2 in H10;Assumption.
-Unfold Rabsolu;Case (case_Rabsolu (Rplus R1 R1));Auto.
- Intro;Cut (Rlt R0 (Rplus R1 R1)).
-Intro;Generalize (Rlt_antisym R0 (Rplus R1 R1) H7);Intro;ElimType False;
- Auto.
-Fourier.
-Apply Rabsolu_no_R0.
-DiscrR.
+ split with (Rmin (Rmin (/ 2) x) (eps * / Rabs (2 * d x0))); split.
+cut (Rmin (/ 2) x > 0).
+cut (eps * / Rabs (2 * d x0) > 0).
+intros; elim (Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) 0);
+ intros a b; apply (b (conj H4 H3)).
+apply Rmult_gt_0_compat; auto.
+unfold Rgt in |- *; apply Rinv_0_lt_compat; apply Rabs_pos_lt;
+ apply Rmult_integral_contrapositive; split.
+discrR.
+assumption.
+elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2).
+intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4;
+ apply (b (conj H4 H)).
+fourier.
+intros; elim H3; clear H3; intros;
+ generalize
+  (let (H1, H2) :=
+       Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) (R_dist x1 x0) in
+   H1); unfold Rgt in |- *; intro; elim (H5 H4); clear H5; 
+ intros; generalize (let (H1, H2) := Rmin_Rgt (/ 2) x (R_dist x1 x0) in H1);
+ unfold Rgt in |- *; intro; elim (H7 H5); clear H7; 
+ intros; clear H4 H5; generalize (H1 x1 (conj H3 H8)); 
+ clear H1; intro; unfold D_x in H3; elim H3; intros;
+ generalize (sym_not_eq H5); clear H5; intro H5;
+ generalize (Rminus_eq_contra x1 x0 H5); intro; generalize H1;
+ pattern (d x0) at 1 in |- *;
+ rewrite <- (let (H1, H2) := Rmult_ne (d x0) in H2);
+ rewrite <- (Rinv_l (x1 - x0) H9); unfold R_dist in |- *;
+ unfold Rminus at 1 in |- *; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0)));
+ rewrite (Rmult_comm (/ (x1 - x0) * (x1 - x0)) (d x0));
+ rewrite <- (Ropp_mult_distr_l_reverse (d x0) (/ (x1 - x0) * (x1 - x0)));
+ rewrite (Rmult_comm (- d x0) (/ (x1 - x0) * (x1 - x0)));
+ rewrite (Rmult_assoc (/ (x1 - x0)) (x1 - x0) (- d x0));
+ rewrite <-
+  (Rmult_plus_distr_l (/ (x1 - x0)) (f x1 - f x0) ((x1 - x0) * - d x0))
+  ; rewrite (Rabs_mult (/ (x1 - x0)) (f x1 - f x0 + (x1 - x0) * - d x0));
+ clear H1; intro;
+ generalize
+  (Rmult_lt_compat_l (Rabs (x1 - x0))
+     (Rabs (/ (x1 - x0)) * Rabs (f x1 - f x0 + (x1 - x0) * - d x0)) eps
+     (Rabs_pos_lt (x1 - x0) H9) H1);
+ rewrite <-
+  (Rmult_assoc (Rabs (x1 - x0)) (Rabs (/ (x1 - x0)))
+     (Rabs (f x1 - f x0 + (x1 - x0) * - d x0)));
+ rewrite (Rabs_Rinv (x1 - x0) H9);
+ rewrite (Rinv_r (Rabs (x1 - x0)) (Rabs_no_R0 (x1 - x0) H9));
+ rewrite
+  (let (H1, H2) := Rmult_ne (Rabs (f x1 - f x0 + (x1 - x0) * - d x0)) in H2)
+  ; generalize (Rabs_triang_inv (f x1 - f x0) ((x1 - x0) * d x0)); 
+ intro; rewrite (Rmult_comm (x1 - x0) (- d x0));
+ rewrite (Ropp_mult_distr_l_reverse (d x0) (x1 - x0));
+ fold (f x1 - f x0 - d x0 * (x1 - x0)) in |- *;
+ rewrite (Rmult_comm (x1 - x0) (d x0)) in H10; clear H1; 
+ intro;
+ generalize
+  (Rle_lt_trans (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0)))
+     (Rabs (f x1 - f x0 - d x0 * (x1 - x0))) (Rabs (x1 - x0) * eps) H10 H1);
+ clear H1; intro;
+ generalize
+  (Rplus_lt_compat_l (Rabs (d x0 * (x1 - x0)))
+     (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0))) (
+     Rabs (x1 - x0) * eps) H1); unfold Rminus at 2 in |- *;
+ rewrite (Rplus_comm (Rabs (f x1 - f x0)) (- Rabs (d x0 * (x1 - x0))));
+ rewrite <-
+  (Rplus_assoc (Rabs (d x0 * (x1 - x0))) (- Rabs (d x0 * (x1 - x0)))
+     (Rabs (f x1 - f x0))); rewrite (Rplus_opp_r (Rabs (d x0 * (x1 - x0))));
+ rewrite (let (H1, H2) := Rplus_ne (Rabs (f x1 - f x0)) in H2); 
+ clear H1; intro; cut (Rabs (d x0 * (x1 - x0)) + Rabs (x1 - x0) * eps < eps).
+intro;
+ apply
+  (Rlt_trans (Rabs (f x1 - f x0))
+     (Rabs (d x0 * (x1 - x0)) + Rabs (x1 - x0) * eps) eps H1 H11). 
+clear H1 H5 H3 H10; generalize (Rabs_pos_lt (d x0) H2); intro;
+ unfold Rgt in H0;
+ generalize (Rmult_lt_compat_l eps (R_dist x1 x0) (/ 2) H0 H7); 
+ clear H7; intro;
+ generalize
+  (Rmult_lt_compat_l (Rabs (d x0)) (R_dist x1 x0) (
+     eps * / Rabs (2 * d x0)) H1 H6); clear H6; intro;
+ rewrite (Rmult_comm eps (R_dist x1 x0)) in H3; unfold R_dist in H3, H5;
+ rewrite <- (Rabs_mult (d x0) (x1 - x0)) in H5;
+ rewrite (Rabs_mult 2 (d x0)) in H5; cut (Rabs 2 <> 0).
+intro; fold (Rabs (d x0) > 0) in H1;
+ rewrite
+  (Rinv_mult_distr (Rabs 2) (Rabs (d x0)) H6
+     (Rlt_dichotomy_converse (Rabs (d x0)) 0 (or_intror (Rabs (d x0) < 0) H1)))
+   in H5;
+ rewrite (Rmult_comm (Rabs (d x0)) (eps * (/ Rabs 2 * / Rabs (d x0)))) in H5;
+ rewrite <- (Rmult_assoc eps (/ Rabs 2) (/ Rabs (d x0))) in H5;
+ rewrite (Rmult_assoc (eps * / Rabs 2) (/ Rabs (d x0)) (Rabs (d x0))) in H5;
+ rewrite
+  (Rinv_l (Rabs (d x0))
+     (Rlt_dichotomy_converse (Rabs (d x0)) 0 (or_intror (Rabs (d x0) < 0) H1)))
+   in H5; rewrite (let (H1, H2) := Rmult_ne (eps * / Rabs 2) in H1) in H5;
+ cut (Rabs 2 = 2).
+intro; rewrite H7 in H5;
+ generalize
+  (Rplus_lt_compat (Rabs (d x0 * (x1 - x0))) (eps * / 2)
+     (Rabs (x1 - x0) * eps) (eps * / 2) H5 H3); intro; 
+ rewrite eps2 in H10; assumption.
+unfold Rabs in |- *; case (Rcase_abs 2); auto.
+ intro; cut (0 < 2).
+intro; generalize (Rlt_asym 0 2 H7); intro; elimtype False; auto.
+fourier.
+apply Rabs_no_R0.
+discrR.
 Qed.
 
 
 (*********)
-Lemma Dconst:(D:R->Prop)(y:R)(x0:R)(D_in [x:R]y [x:R]R0 D x0).
-Unfold D_in;Intros;Unfold limit1_in;Unfold limit_in;Unfold Rdiv;Intros;Simpl;
- Split with eps;Split;Auto.
-Intros;Rewrite (eq_Rminus y y (refl_eqT R y));
- Rewrite Rmult_Ol;Unfold R_dist; 
- Rewrite (eq_Rminus R0 R0 (refl_eqT R R0));Unfold Rabsolu;
- Case (case_Rabsolu R0);Intro.
-Absurd (Rlt R0 R0);Auto.
-Red;Intro;Apply (Rlt_antirefl R0 H1).
-Unfold Rgt in H0;Assumption.
+Lemma Dconst :
+ forall (D:R -> Prop) (y x0:R), D_in (fun x:R => y) (fun x:R => 0) D x0.
+unfold D_in in |- *; intros; unfold limit1_in in |- *;
+ unfold limit_in in |- *; unfold Rdiv in |- *; intros; 
+ simpl in |- *; split with eps; split; auto.
+intros; rewrite (Rminus_diag_eq y y (refl_equal y)); rewrite Rmult_0_l;
+ unfold R_dist in |- *; rewrite (Rminus_diag_eq 0 0 (refl_equal 0));
+ unfold Rabs in |- *; case (Rcase_abs 0); intro.
+absurd (0 < 0); auto.
+red in |- *; intro; apply (Rlt_irrefl 0 H1).
+unfold Rgt in H0; assumption.
 Qed.
 
 (*********)
-Lemma Dx:(D:R->Prop)(x0:R)(D_in [x:R]x [x:R]R1 D x0).
-Unfold D_in;Unfold Rdiv;Intros;Unfold limit1_in;Unfold limit_in;Intros;Simpl;
-  Split with eps;Split;Auto.
-Intros;Elim H0;Clear H0;Intros;Unfold D_x in H0;
- Elim H0;Intros;
- Rewrite (Rinv_r (Rminus x x0) (Rminus_eq_contra x x0 
-      (sym_not_eqT R x0 x H3)));
- Unfold R_dist; 
- Rewrite (eq_Rminus R1 R1 (refl_eqT R R1));Unfold Rabsolu;
- Case (case_Rabsolu R0);Intro.
-Absurd (Rlt R0 R0);Auto.
-Red;Intro;Apply (Rlt_antirefl R0 r).
-Unfold Rgt in H;Assumption.
+Lemma Dx :
+ forall (D:R -> Prop) (x0:R), D_in (fun x:R => x) (fun x:R => 1) D x0.
+unfold D_in in |- *; unfold Rdiv in |- *; intros; unfold limit1_in in |- *;
+ unfold limit_in in |- *; intros; simpl in |- *; split with eps; 
+ split; auto.
+intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros;
+ rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3)));
+ unfold R_dist in |- *; rewrite (Rminus_diag_eq 1 1 (refl_equal 1));
+ unfold Rabs in |- *; case (Rcase_abs 0); intro.
+absurd (0 < 0); auto.
+red in |- *; intro; apply (Rlt_irrefl 0 r).
+unfold Rgt in H; assumption.
 Qed. 
 
 (*********)
-Lemma Dadd:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R)
-  (D_in f df D x0)->(D_in g dg D x0)->
-  (D_in [x:R](Rplus (f x) (g x)) [x:R](Rplus (df x) (dg x)) D x0).
-Unfold D_in;Intros;Generalize (limit_plus 
-   [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0)))
-   [x:R](Rmult  (Rminus (g x) (g x0)) (Rinv (Rminus x x0))) 
-   (D_x D x0) (df x0) (dg x0) x0 H H0);Clear H H0;
- Unfold limit1_in;Unfold limit_in;Simpl;Intros;
- Elim (H eps H0);Clear H;Intros;Elim H;Clear H;Intros;
- Split with x;Split;Auto;Intros;Generalize (H1 x1 H2);Clear H1;Intro; 
- Rewrite (Rmult_sym (Rminus (f x1) (f x0)) (Rinv (Rminus x1 x0))) in H1;
- Rewrite (Rmult_sym (Rminus (g x1) (g x0)) (Rinv (Rminus x1 x0))) in H1;
- Rewrite <-(Rmult_Rplus_distr (Rinv (Rminus x1 x0)) 
-                    (Rminus (f x1) (f x0)) 
-                    (Rminus (g x1) (g x0))) in H1;
- Rewrite (Rmult_sym (Rinv (Rminus x1 x0))
-           (Rplus (Rminus (f x1) (f x0)) (Rminus (g x1) (g x0)))) in H1;
- Cut (Rplus (Rminus (f x1) (f x0)) (Rminus (g x1) (g x0)))==
-      (Rminus (Rplus (f x1) (g x1)) (Rplus (f x0) (g x0))).
-Intro;Rewrite H3 in H1;Assumption.
-Ring.
+Lemma Dadd :
+ forall (D:R -> Prop) (df dg f g:R -> R) (x0:R),
+   D_in f df D x0 ->
+   D_in g dg D x0 ->
+   D_in (fun x:R => f x + g x) (fun x:R => df x + dg x) D x0.
+unfold D_in in |- *; intros;
+ generalize
+  (limit_plus (fun x:R => (f x - f x0) * / (x - x0))
+     (fun x:R => (g x - g x0) * / (x - x0)) (D_x D x0) (
+     df x0) (dg x0) x0 H H0); clear H H0; unfold limit1_in in |- *;
+ unfold limit_in in |- *; simpl in |- *; intros; elim (H eps H0); 
+ clear H; intros; elim H; clear H; intros; split with x; 
+ split; auto; intros; generalize (H1 x1 H2); clear H1; 
+ intro; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1;
+ rewrite (Rmult_comm (g x1 - g x0) (/ (x1 - x0))) in H1;
+ rewrite <- (Rmult_plus_distr_l (/ (x1 - x0)) (f x1 - f x0) (g x1 - g x0))
+   in H1;
+ rewrite (Rmult_comm (/ (x1 - x0)) (f x1 - f x0 + (g x1 - g x0))) in H1;
+ cut (f x1 - f x0 + (g x1 - g x0) = f x1 + g x1 - (f x0 + g x0)).
+intro; rewrite H3 in H1; assumption.
+ring.
 Qed.
 
 (*********)
-Lemma Dmult:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R)
-  (D_in f df D x0)->(D_in g dg D x0)->
-  (D_in [x:R](Rmult (f x) (g x))  
-             [x:R](Rplus (Rmult (df x) (g x)) (Rmult (f x) (dg x))) D x0).
-Intros;Unfold D_in;Generalize H H0;Intros;Unfold D_in in H H0;
- Generalize (cont_deriv f df D x0 H1);Unfold continue_in;Intro;
- Generalize (limit_mul 
-   [x:R](Rmult (Rminus (g x) (g x0)) (Rinv (Rminus x x0)))
-   [x:R](f x) (D_x D x0) (dg x0) (f x0) x0 H0 H3);Intro;
- Cut (limit1_in [x:R](g x0) (D_x D x0) (g x0) x0).
-Intro;Generalize (limit_mul 
-  [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0)))
-  [_:R](g x0) (D_x D x0) (df x0) (g x0) x0 H H5);Clear H H0 H1 H2 H3 H5;
- Intro;Generalize (limit_plus 
-  [x:R](Rmult (Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0))) (g x0))
-  [x:R](Rmult (Rmult (Rminus (g x) (g x0)) (Rinv (Rminus x x0)))
-                (f x)) (D_x D x0) (Rmult (df x0) (g x0)) 
-                               (Rmult (dg x0) (f x0)) x0 H H4);
- Clear H4 H;Intro;Unfold limit1_in in H;Unfold limit_in in H;
- Simpl in H;Unfold limit1_in;Unfold limit_in;Simpl;Intros;
- Elim (H eps H0);Clear H;Intros;Elim H;Clear H;Intros;
- Split with x;Split;Auto;Intros;Generalize (H1 x1 H2);Clear H1;Intro;
- Rewrite (Rmult_sym (Rminus (f x1) (f x0)) (Rinv (Rminus x1 x0))) in H1;
- Rewrite (Rmult_sym (Rminus (g x1) (g x0)) (Rinv (Rminus x1 x0))) in H1;
- Rewrite (Rmult_assoc (Rinv (Rminus x1 x0)) (Rminus (f x1) (f x0))
-       (g x0)) in H1;
- Rewrite (Rmult_assoc (Rinv (Rminus x1 x0)) (Rminus (g x1) (g x0))
-       (f x1)) in H1;
- Rewrite <-(Rmult_Rplus_distr (Rinv (Rminus x1 x0))
-                (Rmult (Rminus (f x1) (f x0)) (g x0))
-                (Rmult (Rminus (g x1) (g x0)) (f x1))) in H1;
- Rewrite (Rmult_sym (Rinv (Rminus x1 x0))
-       (Rplus (Rmult (Rminus (f x1) (f x0)) (g x0))
-               (Rmult (Rminus (g x1) (g x0)) (f x1)))) in H1;
- Rewrite (Rmult_sym (dg x0) (f x0)) in H1;
- Cut (Rplus (Rmult (Rminus (f x1) (f x0)) (g x0))
-               (Rmult (Rminus (g x1) (g x0)) (f x1)))==
-      (Rminus (Rmult (f x1) (g x1)) (Rmult (f x0) (g x0))).
-Intro;Rewrite H3 in H1;Assumption.
-Ring.
-Unfold limit1_in;Unfold limit_in;Simpl;Intros;
- Split with eps;Split;Auto;Intros;Elim (R_dist_refl (g x0) (g x0));
- Intros a b;Rewrite (b (refl_eqT R (g x0)));Unfold Rgt in H;Assumption.
+Lemma Dmult :
+ forall (D:R -> Prop) (df dg f g:R -> R) (x0:R),
+   D_in f df D x0 ->
+   D_in g dg D x0 ->
+   D_in (fun x:R => f x * g x) (fun x:R => df x * g x + f x * dg x) D x0.
+intros; unfold D_in in |- *; generalize H H0; intros; unfold D_in in H, H0;
+ generalize (cont_deriv f df D x0 H1); unfold continue_in in |- *; 
+ intro;
+ generalize
+  (limit_mul (fun x:R => (g x - g x0) * / (x - x0)) (
+     fun x:R => f x) (D_x D x0) (dg x0) (f x0) x0 H0 H3); 
+ intro; cut (limit1_in (fun x:R => g x0) (D_x D x0) (g x0) x0).
+intro;
+ generalize
+  (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) (
+     fun _:R => g x0) (D_x D x0) (df x0) (g x0) x0 H H5);
+ clear H H0 H1 H2 H3 H5; intro;
+ generalize
+  (limit_plus (fun x:R => (f x - f x0) * / (x - x0) * g x0)
+     (fun x:R => (g x - g x0) * / (x - x0) * f x) (
+     D_x D x0) (df x0 * g x0) (dg x0 * f x0) x0 H H4); 
+ clear H4 H; intro; unfold limit1_in in H; unfold limit_in in H; 
+ simpl in H; unfold limit1_in in |- *; unfold limit_in in |- *; 
+ simpl in |- *; intros; elim (H eps H0); clear H; intros; 
+ elim H; clear H; intros; split with x; split; auto; 
+ intros; generalize (H1 x1 H2); clear H1; intro;
+ rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1;
+ rewrite (Rmult_comm (g x1 - g x0) (/ (x1 - x0))) in H1;
+ rewrite (Rmult_assoc (/ (x1 - x0)) (f x1 - f x0) (g x0)) in H1;
+ rewrite (Rmult_assoc (/ (x1 - x0)) (g x1 - g x0) (f x1)) in H1;
+ rewrite <-
+  (Rmult_plus_distr_l (/ (x1 - x0)) ((f x1 - f x0) * g x0)
+     ((g x1 - g x0) * f x1)) in H1;
+ rewrite
+  (Rmult_comm (/ (x1 - x0)) ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1))
+   in H1; rewrite (Rmult_comm (dg x0) (f x0)) in H1;
+ cut
+  ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1 = f x1 * g x1 - f x0 * g x0).
+intro; rewrite H3 in H1; assumption.
+ring.
+unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
+ split with eps; split; auto; intros; elim (R_dist_refl (g x0) (g x0));
+ intros a b; rewrite (b (refl_equal (g x0))); unfold Rgt in H; 
+ assumption.
 Qed.
 
 (*********)
-Lemma Dmult_const:(D:R->Prop)(f,df:R->R)(x0:R)(a:R)(D_in f df D x0)->
-  (D_in [x:R](Rmult a (f x)) ([x:R](Rmult a (df x))) D x0).
-Intros;Generalize (Dmult D [_:R]R0 df [_:R]a f x0 (Dconst D a x0) H);
- Unfold D_in;Intros;
- Rewrite (Rmult_Ol (f x0)) in H0;
- Rewrite (let (H1,H2)=(Rplus_ne (Rmult a (df x0))) in H2) in H0;
- Assumption.
+Lemma Dmult_const :
+ forall (D:R -> Prop) (f df:R -> R) (x0 a:R),
+   D_in f df D x0 -> D_in (fun x:R => a * f x) (fun x:R => a * df x) D x0.
+intros;
+ generalize (Dmult D (fun _:R => 0) df (fun _:R => a) f x0 (Dconst D a x0) H);
+ unfold D_in in |- *; intros; rewrite (Rmult_0_l (f x0)) in H0;
+ rewrite (let (H1, H2) := Rplus_ne (a * df x0) in H2) in H0; 
+ assumption.
 Qed.
 
 (*********)
-Lemma Dopp:(D:R->Prop)(f,df:R->R)(x0:R)(D_in f df D x0)->
-  (D_in [x:R](Ropp (f x)) ([x:R](Ropp (df x))) D x0).
-Intros;Generalize (Dmult_const D f df x0 (Ropp R1) H); Unfold D_in;
- Unfold limit1_in;Unfold limit_in;Intros;
- Generalize (H0 eps H1);Clear H0;Intro;Elim H0;Clear H0;Intros; 
- Elim H0;Clear H0;Simpl;Intros;Split with x;Split;Auto.
-Intros;Generalize (H2 x1 H3);Clear H2;Intro;Rewrite Ropp_mul1 in H2;
- Rewrite Ropp_mul1 in H2;Rewrite Ropp_mul1 in H2;
- Rewrite (let (H1,H2)=(Rmult_ne (f x1)) in H2) in H2; 
- Rewrite (let (H1,H2)=(Rmult_ne (f x0)) in H2) in H2;
- Rewrite (let (H1,H2)=(Rmult_ne (df x0)) in H2) in H2;Assumption.
+Lemma Dopp :
+ forall (D:R -> Prop) (f df:R -> R) (x0:R),
+   D_in f df D x0 -> D_in (fun x:R => - f x) (fun x:R => - df x) D x0.
+intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in in |- *;
+ unfold limit1_in in |- *; unfold limit_in in |- *; 
+ intros; generalize (H0 eps H1); clear H0; intro; elim H0; 
+ clear H0; intros; elim H0; clear H0; simpl in |- *; 
+ intros; split with x; split; auto.
+intros; generalize (H2 x1 H3); clear H2; intro;
+ rewrite Ropp_mult_distr_l_reverse in H2;
+ rewrite Ropp_mult_distr_l_reverse in H2;
+ rewrite Ropp_mult_distr_l_reverse in H2;
+ rewrite (let (H1, H2) := Rmult_ne (f x1) in H2) in H2;
+ rewrite (let (H1, H2) := Rmult_ne (f x0) in H2) in H2;
+ rewrite (let (H1, H2) := Rmult_ne (df x0) in H2) in H2; 
+ assumption.
 Qed.
 
 (*********)
-Lemma Dminus:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R)
-  (D_in f df D x0)->(D_in g dg D x0)->
-  (D_in [x:R](Rminus (f x) (g x)) [x:R](Rminus (df x) (dg x)) D x0).
-Unfold Rminus;Intros;Generalize (Dopp D g dg x0 H0);Intro;
- Apply (Dadd D df [x:R](Ropp (dg x)) f [x:R](Ropp (g x)) x0);Assumption. 
+Lemma Dminus :
+ forall (D:R -> Prop) (df dg f g:R -> R) (x0:R),
+   D_in f df D x0 ->
+   D_in g dg D x0 ->
+   D_in (fun x:R => f x - g x) (fun x:R => df x - dg x) D x0.
+unfold Rminus in |- *; intros; generalize (Dopp D g dg x0 H0); intro;
+ apply (Dadd D df (fun x:R => - dg x) f (fun x:R => - g x) x0); 
+ assumption. 
 Qed.
 
 (*********)
-Lemma Dx_pow_n:(n:nat)(D:R->Prop)(x0:R)
-  (D_in [x:R](pow x n)  
-        [x:R](Rmult (INR n) (pow x (minus n (1)))) D x0).
-Induction n;Intros.
-Simpl; Rewrite Rmult_Ol; Apply Dconst.
-Intros;Cut n0=(minus (S n0) (1));
-  [ Intro a; Rewrite <- a;Clear a | Simpl; Apply minus_n_O ].
-Generalize (Dmult D [_:R]R1 
-   [x:R](Rmult (INR n0) (pow x (minus n0 (1)))) [x:R]x [x:R](pow x n0) 
-   x0 (Dx D x0) (H D x0));Unfold D_in;Unfold limit1_in;Unfold limit_in;
- Simpl;Intros;
- Elim (H0 eps H1);Clear H0;Intros;Elim H0;Clear H0;Intros;
- Split with x;Split;Auto.
-Intros;Generalize (H2 x1 H3);Clear H2 H3;Intro;
- Rewrite (let (H1,H2)=(Rmult_ne (pow x0 n0)) in H2) in H2;
- Rewrite (tech_pow_Rmult x1 n0) in H2;
- Rewrite (tech_pow_Rmult x0 n0) in H2;
- Rewrite (Rmult_sym (INR n0) (pow x0 (minus n0 (1)))) in H2;
- Rewrite <-(Rmult_assoc x0 (pow x0 (minus n0 (1))) (INR n0)) in H2;
- Rewrite (tech_pow_Rmult x0 (minus n0 (1))) in H2;
- Elim (classic (n0=O));Intro cond.
-Rewrite cond in H2;Rewrite cond;Simpl in H2;Simpl;
- Cut (Rplus R1 (Rmult (Rmult x0 R1) R0))==(Rmult R1 R1);
- [Intro A; Rewrite A in H2; Assumption|Ring].
-Cut ~(n0=O)->(S (minus n0 (1)))=n0;[Intro|Omega];
- Rewrite (H3 cond) in H2; Rewrite (Rmult_sym (pow x0 n0) (INR n0)) in H2;
- Rewrite (tech_pow_Rplus x0 n0 n0) in H2; Assumption.
+Lemma Dx_pow_n :
+ forall (n:nat) (D:R -> Prop) (x0:R),
+   D_in (fun x:R => x ^ n) (fun x:R => INR n * x ^ (n - 1)) D x0.
+simple induction n; intros.
+simpl in |- *; rewrite Rmult_0_l; apply Dconst.
+intros; cut (n0 = (S n0 - 1)%nat);
+ [ intro a; rewrite <- a; clear a | simpl in |- *; apply minus_n_O ].
+generalize
+ (Dmult D (fun _:R => 1) (fun x:R => INR n0 * x ^ (n0 - 1)) (
+    fun x:R => x) (fun x:R => x ^ n0) x0 (Dx D x0) (
+    H D x0)); unfold D_in in |- *; unfold limit1_in in |- *;
+ unfold limit_in in |- *; simpl in |- *; intros; elim (H0 eps H1); 
+ clear H0; intros; elim H0; clear H0; intros; split with x; 
+ split; auto.
+intros; generalize (H2 x1 H3); clear H2 H3; intro;
+ rewrite (let (H1, H2) := Rmult_ne (x0 ^ n0) in H2) in H2;
+ rewrite (tech_pow_Rmult x1 n0) in H2; rewrite (tech_pow_Rmult x0 n0) in H2;
+ rewrite (Rmult_comm (INR n0) (x0 ^ (n0 - 1))) in H2;
+ rewrite <- (Rmult_assoc x0 (x0 ^ (n0 - 1)) (INR n0)) in H2;
+ rewrite (tech_pow_Rmult x0 (n0 - 1)) in H2; elim (classic (n0 = 0%nat));
+ intro cond.
+rewrite cond in H2; rewrite cond; simpl in H2; simpl in |- *;
+ cut (1 + x0 * 1 * 0 = 1 * 1);
+ [ intro A; rewrite A in H2; assumption | ring ].
+cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | omega ];
+ rewrite (H3 cond) in H2; rewrite (Rmult_comm (x0 ^ n0) (INR n0)) in H2;
+ rewrite (tech_pow_Rplus x0 n0 n0) in H2; assumption.
 Qed.
 
 (*********)
-Lemma Dcomp:(Df,Dg:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R)
-  (D_in f df Df x0)->(D_in g dg Dg (f x0))->
-  (D_in [x:R](g (f x)) [x:R](Rmult (df x) (dg (f x))) 
-                       (Dgf Df Dg f) x0).
-Intros Df Dg df dg f g x0 H H0;Generalize H H0;Unfold D_in;Unfold Rdiv;Intros;
-Generalize (limit_comp f [x:R](Rmult (Rminus (g x) (g (f x0)))
-                               (Rinv (Rminus x (f x0)))) (D_x Df x0)
-              (D_x Dg (f x0)) 
-              (f x0) (dg (f x0)) x0);Intro;
- Generalize (cont_deriv f df Df x0 H);Intro;Unfold continue_in in H4;
- Generalize (H3 H4 H2);Clear H3;Intro;
- Generalize (limit_mul [x:R](Rmult (Rminus (g (f x)) (g (f x0)))
-                                   (Rinv (Rminus (f x) (f x0))))
-                       [x:R](Rmult (Rminus (f x) (f x0))
-                                   (Rinv (Rminus x x0))) 
-                       (Dgf (D_x Df x0) (D_x Dg (f x0)) f) 
-                       (dg (f x0)) (df x0) x0 H3);Intro;
- Cut (limit1_in
-         [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0)))
-         (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (df x0) x0).
-Intro;Generalize (H5 H6);Clear H5;Intro;
- Generalize (limit_mul 
-        [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0))) 
-        [x:R](dg (f x0))
-       (D_x Df x0) (df x0) (dg (f x0)) x0 H1
-    (limit_free [x:R](dg (f x0)) (D_x Df x0) x0 x0));
- Intro;
- Unfold limit1_in;Unfold limit_in;Simpl;Unfold limit1_in in H5 H7;
- Unfold limit_in in H5 H7;Simpl in H5 H7;Intros;Elim (H5 eps H8);
- Elim (H7 eps H8);Clear H5 H7;Intros;Elim H5;Elim H7;Clear H5 H7;
- Intros;Split with (Rmin x x1);Split.
-Elim (Rmin_Rgt x x1 R0);Intros a b;
- Apply (b (conj (Rgt x R0) (Rgt x1 R0) H9 H5));Clear a b.
-Intros;Elim H11;Clear H11;Intros;Elim (Rmin_Rgt x x1 (R_dist x2 x0));
- Intros a b;Clear b;Unfold Rgt in a;Elim (a H12);Clear H5 a;Intros;
- Unfold D_x Dgf in H11 H7 H10;Clear H12;
- Elim (classic (f x2)==(f x0));Intro.
-Elim H11;Clear H11;Intros;Elim H11;Clear H11;Intros;
- Generalize (H10 x2 (conj (Df x2)/\~x0==x2 (Rlt (R_dist x2 x0) x)
-        (conj (Df x2) ~x0==x2 H11 H14) H5));Intro;
- Rewrite (eq_Rminus (f x2) (f x0) H12) in H16;
- Rewrite (Rmult_Ol (Rinv (Rminus x2 x0))) in H16;
- Rewrite (Rmult_Ol (dg (f x0))) in H16;
- Rewrite H12;
- Rewrite (eq_Rminus (g (f x0)) (g (f x0)) (refl_eqT R (g (f x0))));
- Rewrite (Rmult_Ol (Rinv (Rminus x2 x0)));Assumption.
-Clear H10 H5;Elim H11;Clear H11;Intros;Elim H5;Clear H5;Intros;
-Cut (((Df x2)/\~x0==x2)/\(Dg (f x2))/\~(f x0)==(f x2))
-        /\(Rlt (R_dist x2 x0) x1);Auto;Intro;
- Generalize (H7 x2 H14);Intro;
- Generalize (Rminus_eq_contra (f x2) (f x0) H12);Intro;
- Rewrite (Rmult_assoc (Rminus (g (f x2)) (g (f x0))) 
-           (Rinv (Rminus (f x2) (f x0)))
-          (Rmult (Rminus (f x2) (f x0)) (Rinv (Rminus x2 x0)))) in H15;
- Rewrite <-(Rmult_assoc (Rinv (Rminus (f x2) (f x0))) 
-             (Rminus (f x2) (f x0)) (Rinv (Rminus x2 x0))) in H15;
- Rewrite (Rinv_l (Rminus (f x2) (f x0)) H16) in H15;
- Rewrite (let (H1,H2)=(Rmult_ne (Rinv (Rminus x2 x0))) in H2) in H15;
- Rewrite (Rmult_sym (df x0) (dg (f x0)));Assumption.
-Clear H5 H3 H4 H2;Unfold limit1_in;Unfold limit_in;Simpl;
- Unfold limit1_in in H1;Unfold limit_in in H1;Simpl in H1;Intros;
- Elim (H1 eps H2);Clear H1;Intros;Elim H1;Clear H1;Intros;
- Split with x;Split;Auto;Intros;Unfold D_x Dgf in H4 H3;
- Elim H4;Clear H4;Intros;Elim H4;Clear H4;Intros;
- Exact (H3 x1 (conj (Df x1)/\~x0==x1 (Rlt (R_dist x1 x0) x) H4 H5)).
+Lemma Dcomp :
+ forall (Df Dg:R -> Prop) (df dg f g:R -> R) (x0:R),
+   D_in f df Df x0 ->
+   D_in g dg Dg (f x0) ->
+   D_in (fun x:R => g (f x)) (fun x:R => df x * dg (f x)) (Dgf Df Dg f) x0.
+intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in in |- *;
+ unfold Rdiv in |- *; intros;
+ generalize
+  (limit_comp f (fun x:R => (g x - g (f x0)) * / (x - f x0)) (
+     D_x Df x0) (D_x Dg (f x0)) (f x0) (dg (f x0)) x0); 
+ intro; generalize (cont_deriv f df Df x0 H); intro; 
+ unfold continue_in in H4; generalize (H3 H4 H2); clear H3; 
+ intro;
+ generalize
+  (limit_mul (fun x:R => (g (f x) - g (f x0)) * / (f x - f x0))
+     (fun x:R => (f x - f x0) * / (x - x0))
+     (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (dg (f x0)) (
+     df x0) x0 H3); intro;
+ cut
+  (limit1_in (fun x:R => (f x - f x0) * / (x - x0))
+     (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (df x0) x0).
+intro; generalize (H5 H6); clear H5; intro;
+ generalize
+  (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) (
+     fun x:R => dg (f x0)) (D_x Df x0) (df x0) (dg (f x0)) x0 H1
+     (limit_free (fun x:R => dg (f x0)) (D_x Df x0) x0 x0)); 
+ intro; unfold limit1_in in |- *; unfold limit_in in |- *; 
+ simpl in |- *; unfold limit1_in in H5, H7; unfold limit_in in H5, H7;
+ simpl in H5, H7; intros; elim (H5 eps H8); elim (H7 eps H8); 
+ clear H5 H7; intros; elim H5; elim H7; clear H5 H7; 
+ intros; split with (Rmin x x1); split.
+elim (Rmin_Rgt x x1 0); intros a b; apply (b (conj H9 H5)); clear a b.
+intros; elim H11; clear H11; intros; elim (Rmin_Rgt x x1 (R_dist x2 x0));
+ intros a b; clear b; unfold Rgt in a; elim (a H12); 
+ clear H5 a; intros; unfold D_x, Dgf in H11, H7, H10; 
+ clear H12; elim (classic (f x2 = f x0)); intro.
+elim H11; clear H11; intros; elim H11; clear H11; intros;
+ generalize (H10 x2 (conj (conj H11 H14) H5)); intro;
+ rewrite (Rminus_diag_eq (f x2) (f x0) H12) in H16;
+ rewrite (Rmult_0_l (/ (x2 - x0))) in H16;
+ rewrite (Rmult_0_l (dg (f x0))) in H16; rewrite H12;
+ rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (refl_equal (g (f x0))));
+ rewrite (Rmult_0_l (/ (x2 - x0))); assumption.
+clear H10 H5; elim H11; clear H11; intros; elim H5; clear H5; intros;
+ cut
+  (((Df x2 /\ x0 <> x2) /\ Dg (f x2) /\ f x0 <> f x2) /\ R_dist x2 x0 < x1);
+ auto; intro; generalize (H7 x2 H14); intro;
+ generalize (Rminus_eq_contra (f x2) (f x0) H12); intro;
+ rewrite
+  (Rmult_assoc (g (f x2) - g (f x0)) (/ (f x2 - f x0))
+     ((f x2 - f x0) * / (x2 - x0))) in H15;
+ rewrite <- (Rmult_assoc (/ (f x2 - f x0)) (f x2 - f x0) (/ (x2 - x0)))
+   in H15; rewrite (Rinv_l (f x2 - f x0) H16) in H15;
+ rewrite (let (H1, H2) := Rmult_ne (/ (x2 - x0)) in H2) in H15;
+ rewrite (Rmult_comm (df x0) (dg (f x0))); assumption.
+clear H5 H3 H4 H2; unfold limit1_in in |- *; unfold limit_in in |- *;
+ simpl in |- *; unfold limit1_in in H1; unfold limit_in in H1; 
+ simpl in H1; intros; elim (H1 eps H2); clear H1; intros; 
+ elim H1; clear H1; intros; split with x; split; auto; 
+ intros; unfold D_x, Dgf in H4, H3; elim H4; clear H4; 
+ intros; elim H4; clear H4; intros; exact (H3 x1 (conj H4 H5)).
 Qed.   
 
 (*********)
-Lemma D_pow_n:(n:nat)(D:R->Prop)(x0:R)(expr,dexpr:R->R)
- (D_in expr dexpr D x0)-> (D_in [x:R](pow (expr x) n) 
-     [x:R](Rmult (Rmult (INR n) (pow (expr x) (minus n (1)))) (dexpr x)) 
-          (Dgf D D expr) x0).
-Intros n D x0 expr dexpr H; 
- Generalize (Dcomp D D dexpr [x:R](Rmult (INR n) (pow x (minus n (1)))) 
-         expr [x:R](pow x n) x0  H (Dx_pow_n n D (expr x0)));
- Intro; Unfold D_in; Unfold limit1_in; Unfold limit_in;Simpl;Intros; 
- Unfold D_in in H0; Unfold limit1_in in H0; Unfold limit_in in H0;Simpl in H0;
- Elim (H0 eps H1);Clear H0;Intros;Elim H0;Clear H0;Intros;Split with x;Split;
- Intros; Auto.
-Cut ``((dexpr x0)*((INR n)*(pow (expr x0) (minus n (S O)))))==
-            ((INR n)*(pow (expr x0) (minus n (S O)))*(dexpr x0))``;
- [Intro Rew;Rewrite <- Rew;Exact (H2 x1 H3)|Ring].
+Lemma D_pow_n :
+ forall (n:nat) (D:R -> Prop) (x0:R) (expr dexpr:R -> R),
+   D_in expr dexpr D x0 ->
+   D_in (fun x:R => expr x ^ n)
+     (fun x:R => INR n * expr x ^ (n - 1) * dexpr x) (
+     Dgf D D expr) x0.
+intros n D x0 expr dexpr H;
+ generalize
+  (Dcomp D D dexpr (fun x:R => INR n * x ^ (n - 1)) expr (
+     fun x:R => x ^ n) x0 H (Dx_pow_n n D (expr x0))); 
+ intro; unfold D_in in |- *; unfold limit1_in in |- *;
+ unfold limit_in in |- *; simpl in |- *; intros; unfold D_in in H0;
+ unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; 
+ elim (H0 eps H1); clear H0; intros; elim H0; clear H0; 
+ intros; split with x; split; intros; auto.
+cut
+ (dexpr x0 * (INR n * expr x0 ^ (n - 1)) =
+  INR n * expr x0 ^ (n - 1) * dexpr x0);
+ [ intro Rew; rewrite <- Rew; exact (H2 x1 H3) | ring ].
 Qed.
-