Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 562 insertions, 525 deletions

diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index aa9e9887..cb6c59d5 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -5,8 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
- 
-(*i $Id: Rpower.v 6295 2004-11-12 16:40:39Z gregoire $ i*)
+
+(*i $Id: Rpower.v 9245 2006-10-17 12:53:34Z notin $ i*)
 (*i Due to L.Thery i*) 
 
 (************************************************************)
@@ -25,637 +25,674 @@ Require Import MVT.
 Require Import Ranalysis4. Open Local Scope R_scope.
 
 Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y).
-intros P x y H1 H2; unfold Rmin in |- *; case (Rle_dec x y); intro;
- assumption.
+Proof.
+  intros P x y H1 H2; unfold Rmin in |- *; case (Rle_dec x y); intro;
+    assumption.
 Qed.
 
 Lemma exp_le_3 : exp 1 <= 3.
-assert (exp_1 : exp 1 <> 0).
-assert (H0 := exp_pos 1); red in |- *; intro; rewrite H in H0;
- elim (Rlt_irrefl _ H0).
-apply Rmult_le_reg_l with (/ exp 1).
-apply Rinv_0_lt_compat; apply exp_pos.
-rewrite <- Rinv_l_sym.
-apply Rmult_le_reg_l with (/ 3).
-apply Rinv_0_lt_compat; prove_sup0.
-rewrite Rmult_1_r; rewrite <- (Rmult_comm 3); rewrite <- Rmult_assoc;
- rewrite <- Rinv_l_sym.
-rewrite Rmult_1_l; replace (/ exp 1) with (exp (-1)).
-unfold exp in |- *; case (exist_exp (-1)); intros; simpl in |- *;
- unfold exp_in in e;
- assert (H := alternated_series_ineq (fun i:nat => / INR (fact i)) x 1).
-cut
- (sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (S (2 * 1)) <= x <=
-  sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (2 * 1)).
-intro; elim H0; clear H0; intros H0 _; simpl in H0; unfold tg_alt in H0;
- simpl in H0.
-replace (/ 3) with
- (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 +
-  -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)).
-apply H0.
-repeat rewrite Rinv_1; repeat rewrite Rmult_1_r;
- rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l;
- rewrite Ropp_involutive; rewrite Rplus_opp_r; rewrite Rmult_1_r;
- rewrite Rplus_0_l; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 6.
-rewrite Rmult_plus_distr_l; replace (2 + 1 + 1 + 1 + 1) with 6.
-rewrite <- (Rmult_comm (/ 6)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
-rewrite Rmult_1_l; replace 6 with 6.
-do 2 rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
-rewrite Rmult_1_r; rewrite (Rmult_comm 3); rewrite <- Rmult_assoc;
- rewrite <- Rinv_r_sym.
-ring.
-discrR.
-discrR.
-ring.
-discrR.
-ring.
-discrR.
-apply H.
-unfold Un_decreasing in |- *; intros;
- apply Rmult_le_reg_l with (INR (fact n)).
-apply INR_fact_lt_0.
-apply Rmult_le_reg_l with (INR (fact (S n))).
-apply INR_fact_lt_0.
-rewrite <- Rinv_r_sym.
-rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc;
- rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; apply le_INR; apply fact_le; apply le_n_Sn.
-apply INR_fact_neq_0.
-apply INR_fact_neq_0.
-assert (H0 := cv_speed_pow_fact 1); unfold Un_cv in |- *; unfold Un_cv in H0;
- intros; elim (H0 _ H1); intros; exists x0; intros; 
- unfold R_dist in H2; unfold R_dist in |- *;
- replace (/ INR (fact n)) with (1 ^ n / INR (fact n)).
-apply (H2 _ H3).
-unfold Rdiv in |- *; rewrite pow1; rewrite Rmult_1_l; reflexivity.
-unfold infinit_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0);
- intros; exists x0; intros;
- replace (sum_f_R0 (fun i:nat => (-1) ^ i * / INR (fact i)) n) with
-  (sum_f_R0 (fun i:nat => / INR (fact i) * (-1) ^ i) n).
-apply (H1 _ H2).
-apply sum_eq; intros; apply Rmult_comm.
-apply Rmult_eq_reg_l with (exp 1).
-rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0;
- rewrite <- Rinv_r_sym.
-reflexivity.
-assumption.
-assumption.
-discrR.
-assumption.
+Proof.
+  assert (exp_1 : exp 1 <> 0).
+  assert (H0 := exp_pos 1); red in |- *; intro; rewrite H in H0;
+    elim (Rlt_irrefl _ H0).
+  apply Rmult_le_reg_l with (/ exp 1).
+  apply Rinv_0_lt_compat; apply exp_pos.
+  rewrite <- Rinv_l_sym.
+  apply Rmult_le_reg_l with (/ 3).
+  apply Rinv_0_lt_compat; prove_sup0.
+  rewrite Rmult_1_r; rewrite <- (Rmult_comm 3); rewrite <- Rmult_assoc;
+    rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_l; replace (/ exp 1) with (exp (-1)).
+  unfold exp in |- *; case (exist_exp (-1)); intros; simpl in |- *;
+    unfold exp_in in e;
+      assert (H := alternated_series_ineq (fun i:nat => / INR (fact i)) x 1).
+  cut
+    (sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (S (2 * 1)) <= x <=
+      sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (2 * 1)).
+  intro; elim H0; clear H0; intros H0 _; simpl in H0; unfold tg_alt in H0;
+    simpl in H0.
+  replace (/ 3) with
+  (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 +
+    -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)).
+  apply H0.
+  repeat rewrite Rinv_1; repeat rewrite Rmult_1_r;
+    rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l;
+      rewrite Ropp_involutive; rewrite Rplus_opp_r; rewrite Rmult_1_r;
+        rewrite Rplus_0_l; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 6.
+  rewrite Rmult_plus_distr_l; replace (2 + 1 + 1 + 1 + 1) with 6.
+  rewrite <- (Rmult_comm (/ 6)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_l; replace 6 with 6.
+  do 2 rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_r; rewrite (Rmult_comm 3); rewrite <- Rmult_assoc;
+    rewrite <- Rinv_r_sym.
+  ring.
+  discrR.
+  discrR.
+  ring.
+  discrR.
+  ring.
+  discrR.
+  apply H.
+  unfold Un_decreasing in |- *; intros;
+    apply Rmult_le_reg_l with (INR (fact n)).
+  apply INR_fact_lt_0.
+  apply Rmult_le_reg_l with (INR (fact (S n))).
+  apply INR_fact_lt_0.
+  rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc;
+    rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; apply le_INR; apply fact_le; apply le_n_Sn.
+  apply INR_fact_neq_0.
+  apply INR_fact_neq_0.
+  assert (H0 := cv_speed_pow_fact 1); unfold Un_cv in |- *; unfold Un_cv in H0;
+    intros; elim (H0 _ H1); intros; exists x0; intros; 
+      unfold R_dist in H2; unfold R_dist in |- *;
+        replace (/ INR (fact n)) with (1 ^ n / INR (fact n)).
+  apply (H2 _ H3).
+  unfold Rdiv in |- *; rewrite pow1; rewrite Rmult_1_l; reflexivity.
+  unfold infinit_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0);
+    intros; exists x0; intros;
+      replace (sum_f_R0 (fun i:nat => (-1) ^ i * / INR (fact i)) n) with
+      (sum_f_R0 (fun i:nat => / INR (fact i) * (-1) ^ i) n).
+  apply (H1 _ H2).
+  apply sum_eq; intros; apply Rmult_comm.
+  apply Rmult_eq_reg_l with (exp 1).
+  rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0;
+    rewrite <- Rinv_r_sym.
+  reflexivity.
+  assumption.
+  assumption.
+  discrR.
+  assumption.
 Qed.
 
 (******************************************************************)
-(*                        Properties of  Exp                      *)
+(** *                     Properties of  Exp                      *)
 (******************************************************************)
 
 Theorem exp_increasing : forall x y:R, x < y -> exp x < exp y.
-intros x y H.
-assert (H0 : derivable exp).
-apply derivable_exp.
-assert (H1 := positive_derivative _ H0).
-unfold strict_increasing in H1.
-apply H1.
-intro.
-replace (derive_pt exp x0 (H0 x0)) with (exp x0).
-apply exp_pos.
-symmetry  in |- *; apply derive_pt_eq_0.
-apply (derivable_pt_lim_exp x0).
-apply H.
-Qed.
- 
+Proof.
+  intros x y H.
+  assert (H0 : derivable exp).
+  apply derivable_exp.
+  assert (H1 := positive_derivative _ H0).
+  unfold strict_increasing in H1.
+  apply H1.
+  intro.
+  replace (derive_pt exp x0 (H0 x0)) with (exp x0).
+  apply exp_pos.
+  symmetry  in |- *; apply derive_pt_eq_0.
+  apply (derivable_pt_lim_exp x0).
+  apply H.
+Qed.
+
 Theorem exp_lt_inv : forall x y:R, exp x < exp y -> x < y.
-intros x y H; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ].
-assumption.
-rewrite H1 in H; elim (Rlt_irrefl _ H).
-assert (H2 := exp_increasing _ _ H1).
-elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H2)).
+Proof.
+  intros x y H; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ].
+  assumption.
+  rewrite H1 in H; elim (Rlt_irrefl _ H).
+  assert (H2 := exp_increasing _ _ H1).
+  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H2)).
 Qed.
- 
+
 Lemma exp_ineq1 : forall x:R, 0 < x -> 1 + x < exp x.
-intros; apply Rplus_lt_reg_r with (- exp 0); rewrite <- (Rplus_comm (exp x));
- assert (H0 := MVT_cor1 exp 0 x derivable_exp H); elim H0; 
- intros; elim H1; intros; unfold Rminus in H2; rewrite H2; 
- rewrite Ropp_0; rewrite Rplus_0_r;
- replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0).
-rewrite exp_0; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
- pattern x at 1 in |- *; rewrite <- Rmult_1_r; rewrite (Rmult_comm (exp x0));
- apply Rmult_lt_compat_l.
-apply H.
-rewrite <- exp_0; apply exp_increasing; elim H3; intros; assumption.
-symmetry  in |- *; apply derive_pt_eq_0; apply derivable_pt_lim_exp.
+Proof.
+  intros; apply Rplus_lt_reg_r with (- exp 0); rewrite <- (Rplus_comm (exp x));
+    assert (H0 := MVT_cor1 exp 0 x derivable_exp H); elim H0; 
+      intros; elim H1; intros; unfold Rminus in H2; rewrite H2; 
+        rewrite Ropp_0; rewrite Rplus_0_r;
+          replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0).
+  rewrite exp_0; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
+    pattern x at 1 in |- *; rewrite <- Rmult_1_r; rewrite (Rmult_comm (exp x0));
+      apply Rmult_lt_compat_l.
+  apply H.
+  rewrite <- exp_0; apply exp_increasing; elim H3; intros; assumption.
+  symmetry  in |- *; apply derive_pt_eq_0; apply derivable_pt_lim_exp.
 Qed.
 
 Lemma ln_exists1 : forall y:R, 0 < y -> 1 <= y -> sigT (fun z:R => y = exp z).
-intros; set (f := fun x:R => exp x - y); cut (f 0 <= 0).
-intro; cut (continuity f).
-intro; cut (0 <= f y).
-intro; cut (f 0 * f y <= 0).
-intro; assert (X := IVT_cor f 0 y H2 (Rlt_le _ _ H) H4); elim X; intros t H5;
- apply existT with t; elim H5; intros; unfold f in H7;
- apply Rminus_diag_uniq_sym; exact H7.
-pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y));
- rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l; 
- assumption.
-unfold f in |- *; apply Rplus_le_reg_l with y; left;
- apply Rlt_trans with (1 + y).
-rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1.
-replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H) | ring ].
-unfold f in |- *; change (continuity (exp - fct_cte y)) in |- *;
- apply continuity_minus;
- [ apply derivable_continuous; apply derivable_exp
- | apply derivable_continuous; apply derivable_const ].
-unfold f in |- *; rewrite exp_0; apply Rplus_le_reg_l with y;
- rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H0 | ring ].
+Proof.
+  intros; set (f := fun x:R => exp x - y); cut (f 0 <= 0).
+  intro; cut (continuity f).
+  intro; cut (0 <= f y).
+  intro; cut (f 0 * f y <= 0).
+  intro; assert (X := IVT_cor f 0 y H2 (Rlt_le _ _ H) H4); elim X; intros t H5;
+    apply existT with t; elim H5; intros; unfold f in H7;
+      apply Rminus_diag_uniq_sym; exact H7.
+  pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y));
+    rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l; 
+      assumption.
+  unfold f in |- *; apply Rplus_le_reg_l with y; left;
+    apply Rlt_trans with (1 + y).
+  rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1.
+  replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H) | ring ].
+  unfold f in |- *; change (continuity (exp - fct_cte y)) in |- *;
+    apply continuity_minus;
+      [ apply derivable_continuous; apply derivable_exp
+        | apply derivable_continuous; apply derivable_const ].
+  unfold f in |- *; rewrite exp_0; apply Rplus_le_reg_l with y;
+    rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H0 | ring ].
 Qed.
 
 (**********)
 Lemma ln_exists : forall y:R, 0 < y -> sigT (fun z:R => y = exp z).
-intros; case (Rle_dec 1 y); intro.
-apply (ln_exists1 _ H r).
-assert (H0 : 1 <= / y).
-apply Rmult_le_reg_l with y.
-apply H.
-rewrite <- Rinv_r_sym.
-rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ n).
-red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
-assert (H1 : 0 < / y).
-apply Rinv_0_lt_compat; apply H.
-assert (H2 := ln_exists1 _ H1 H0); elim H2; intros; apply existT with (- x);
- apply Rmult_eq_reg_l with (exp x / y).
-unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-rewrite Rmult_1_r; rewrite <- (Rmult_comm (/ y)); rewrite Rmult_assoc;
- rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; 
- rewrite Rmult_1_r; symmetry  in |- *; apply p.
-red in |- *; intro; rewrite H3 in H; elim (Rlt_irrefl _ H).
-unfold Rdiv in |- *; apply prod_neq_R0.
-assert (H3 := exp_pos x); red in |- *; intro; rewrite H4 in H3;
- elim (Rlt_irrefl _ H3).
-apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H;
- elim (Rlt_irrefl _ H).
+Proof.
+  intros; case (Rle_dec 1 y); intro.
+  apply (ln_exists1 _ H r).
+  assert (H0 : 1 <= / y).
+  apply Rmult_le_reg_l with y.
+  apply H.
+  rewrite <- Rinv_r_sym.
+  rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ n).
+  red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
+  assert (H1 : 0 < / y).
+  apply Rinv_0_lt_compat; apply H.
+  assert (H2 := ln_exists1 _ H1 H0); elim H2; intros; apply existT with (- x);
+    apply Rmult_eq_reg_l with (exp x / y).
+  unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+  rewrite Rmult_1_r; rewrite <- (Rmult_comm (/ y)); rewrite Rmult_assoc;
+    rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; 
+      rewrite Rmult_1_r; symmetry  in |- *; apply p.
+  red in |- *; intro; rewrite H3 in H; elim (Rlt_irrefl _ H).
+  unfold Rdiv in |- *; apply prod_neq_R0.
+  assert (H3 := exp_pos x); red in |- *; intro; rewrite H4 in H3;
+    elim (Rlt_irrefl _ H3).
+  apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H;
+    elim (Rlt_irrefl _ H).
 Qed.
 
 (* Definition of log R+* -> R *)
 Definition Rln (y:posreal) : R :=
   match ln_exists (pos y) (cond_pos y) with
-  | existT a b => a
+    | existT a b => a
   end.
 
 (* Extension on R *)
 Definition ln (x:R) : R :=
   match Rlt_dec 0 x with
-  | left a => Rln (mkposreal x a)
-  | right a => 0
+    | left a => Rln (mkposreal x a)
+    | right a => 0
   end.
 
 Lemma exp_ln : forall x:R, 0 < x -> exp (ln x) = x.
-intros; unfold ln in |- *; case (Rlt_dec 0 x); intro.
-unfold Rln in |- *;
- case (ln_exists (mkposreal x r) (cond_pos (mkposreal x r))); 
- intros.
-simpl in e; symmetry  in |- *; apply e.
-elim n; apply H.
+Proof.
+  intros; unfold ln in |- *; case (Rlt_dec 0 x); intro.
+  unfold Rln in |- *;
+    case (ln_exists (mkposreal x r) (cond_pos (mkposreal x r))); 
+    intros.
+  simpl in e; symmetry  in |- *; apply e.
+  elim n; apply H.
 Qed.
 
 Theorem exp_inv : forall x y:R, exp x = exp y -> x = y.
-intros x y H; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ]; auto;
- assert (H2 := exp_increasing _ _ H1); rewrite H in H2;
- elim (Rlt_irrefl _ H2).
+Proof.
+  intros x y H; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ]; auto;
+    assert (H2 := exp_increasing _ _ H1); rewrite H in H2;
+      elim (Rlt_irrefl _ H2).
 Qed.
- 
+
 Theorem exp_Ropp : forall x:R, exp (- x) = / exp x.
-intros x; assert (H : exp x <> 0).
-assert (H := exp_pos x); red in |- *; intro; rewrite H0 in H;
- elim (Rlt_irrefl _ H).
-apply Rmult_eq_reg_l with (r := exp x).
-rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0.
-apply Rinv_r_sym.
-apply H.
-apply H.
-Qed.
- 
+Proof.
+  intros x; assert (H : exp x <> 0).
+  assert (H := exp_pos x); red in |- *; intro; rewrite H0 in H;
+    elim (Rlt_irrefl _ H).
+  apply Rmult_eq_reg_l with (r := exp x).
+  rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0.
+  apply Rinv_r_sym.
+  apply H.
+  apply H.
+Qed.
+
 (******************************************************************)
-(*                        Properties of  Ln                       *)
+(** *                     Properties of  Ln                       *)
 (******************************************************************)
 
 Theorem ln_increasing : forall x y:R, 0 < x -> x < y -> ln x < ln y.
-intros x y H H0; apply exp_lt_inv.
-repeat rewrite exp_ln. 
-apply H0.
-apply Rlt_trans with x; assumption.
-apply H.
+Proof.
+  intros x y H H0; apply exp_lt_inv.
+  repeat rewrite exp_ln. 
+  apply H0.
+  apply Rlt_trans with x; assumption.
+  apply H.
 Qed.
 
 Theorem ln_exp : forall x:R, ln (exp x) = x.
-intros x; apply exp_inv.
-apply exp_ln.
-apply exp_pos.
+Proof.
+  intros x; apply exp_inv.
+  apply exp_ln.
+  apply exp_pos.
 Qed.
- 
+
 Theorem ln_1 : ln 1 = 0.
-rewrite <- exp_0; rewrite ln_exp; reflexivity.
+Proof.
+  rewrite <- exp_0; rewrite ln_exp; reflexivity.
 Qed.
- 
+
 Theorem ln_lt_inv : forall x y:R, 0 < x -> 0 < y -> ln x < ln y -> x < y.
-intros x y H H0 H1; rewrite <- (exp_ln x); try rewrite <- (exp_ln y).
-apply exp_increasing; apply H1.
-assumption. 
-assumption.
+Proof.
+  intros x y H H0 H1; rewrite <- (exp_ln x); try rewrite <- (exp_ln y).
+  apply exp_increasing; apply H1.
+  assumption. 
+  assumption.
 Qed.
- 
+
 Theorem ln_inv : forall x y:R, 0 < x -> 0 < y -> ln x = ln y -> x = y.
-intros x y H H0 H'0; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ];
- auto.
-assert (H2 := ln_increasing _ _ H H1); rewrite H'0 in H2;
- elim (Rlt_irrefl _ H2).
-assert (H2 := ln_increasing _ _ H0 H1); rewrite H'0 in H2;
- elim (Rlt_irrefl _ H2).
-Qed.
- 
+Proof.
+  intros x y H H0 H'0; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ];
+    auto.
+  assert (H2 := ln_increasing _ _ H H1); rewrite H'0 in H2;
+    elim (Rlt_irrefl _ H2).
+  assert (H2 := ln_increasing _ _ H0 H1); rewrite H'0 in H2;
+    elim (Rlt_irrefl _ H2).
+Qed.
+
 Theorem ln_mult : forall x y:R, 0 < x -> 0 < y -> ln (x * y) = ln x + ln y.
-intros x y H H0; apply exp_inv.
-rewrite exp_plus.
-repeat rewrite exp_ln.
-reflexivity.
-assumption.
-assumption.
-apply Rmult_lt_0_compat; assumption.
+Proof.
+  intros x y H H0; apply exp_inv.
+  rewrite exp_plus.
+  repeat rewrite exp_ln.
+  reflexivity.
+  assumption.
+  assumption.
+  apply Rmult_lt_0_compat; assumption.
 Qed.
 
 Theorem ln_Rinv : forall x:R, 0 < x -> ln (/ x) = - ln x.
-intros x H; apply exp_inv; repeat rewrite exp_ln || rewrite exp_Ropp.
-reflexivity.
-assumption. 
-apply Rinv_0_lt_compat; assumption.
+Proof.
+  intros x H; apply exp_inv; repeat rewrite exp_ln || rewrite exp_Ropp.
+  reflexivity.
+  assumption. 
+  apply Rinv_0_lt_compat; assumption.
 Qed.
 
 Theorem ln_continue :
- forall y:R, 0 < y -> continue_in ln (fun x:R => 0 < x) y.
-intros y H.
-unfold continue_in, limit1_in, limit_in in |- *; intros eps Heps.
-cut (1 < exp eps); [ intros H1 | idtac ].
-cut (exp (- eps) < 1); [ intros H2 | idtac ].
-exists (Rmin (y * (exp eps - 1)) (y * (1 - exp (- eps)))); split.
-red in |- *; apply P_Rmin.
-apply Rmult_lt_0_compat.
-assumption.
-apply Rplus_lt_reg_r with 1.
-rewrite Rplus_0_r; replace (1 + (exp eps - 1)) with (exp eps);
- [ apply H1 | ring ].
-apply Rmult_lt_0_compat.
-assumption.
-apply Rplus_lt_reg_r with (exp (- eps)).
-rewrite Rplus_0_r; replace (exp (- eps) + (1 - exp (- eps))) with 1;
- [ apply H2 | ring ].
-unfold dist, R_met, R_dist in |- *; simpl in |- *.
-intros x [[H3 H4] H5].
-cut (y * (x * / y) = x).
-intro Hxyy. 
-replace (ln x - ln y) with (ln (x * / y)).
-case (Rtotal_order x y); [ intros Hxy | intros [Hxy| Hxy] ].
-rewrite Rabs_left.
-apply Ropp_lt_cancel; rewrite Ropp_involutive.
-apply exp_lt_inv.
-rewrite exp_ln.
-apply Rmult_lt_reg_l with (r := y).
-apply H.
-rewrite Hxyy.
-apply Ropp_lt_cancel.
-apply Rplus_lt_reg_r with (r := y).
-replace (y + - (y * exp (- eps))) with (y * (1 - exp (- eps)));
- [ idtac | ring ].
-replace (y + - x) with (Rabs (x - y)); [ idtac | ring ].
-apply Rlt_le_trans with (1 := H5); apply Rmin_r.
-rewrite Rabs_left; [ ring | idtac ].
-apply (Rlt_minus _ _ Hxy).
-apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
-rewrite <- ln_1.
-apply ln_increasing.
-apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
-apply Rmult_lt_reg_l with (r := y).
-apply H.
-rewrite Hxyy; rewrite Rmult_1_r; apply Hxy.
-rewrite Hxy; rewrite Rinv_r.
-rewrite ln_1; rewrite Rabs_R0; apply Heps.
-red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
-rewrite Rabs_right.
-apply exp_lt_inv.
-rewrite exp_ln.
-apply Rmult_lt_reg_l with (r := y).
-apply H.
-rewrite Hxyy.
-apply Rplus_lt_reg_r with (r := - y).
-replace (- y + y * exp eps) with (y * (exp eps - 1)); [ idtac | ring ].
-replace (- y + x) with (Rabs (x - y)); [ idtac | ring ].
-apply Rlt_le_trans with (1 := H5); apply Rmin_l.
-rewrite Rabs_right; [ ring | idtac ].
-left; apply (Rgt_minus _ _ Hxy).
-apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
-rewrite <- ln_1.
-apply Rgt_ge; red in |- *; apply ln_increasing.
-apply Rlt_0_1.
-apply Rmult_lt_reg_l with (r := y).
-apply H.
-rewrite Hxyy; rewrite Rmult_1_r; apply Hxy.
-rewrite ln_mult.
-rewrite ln_Rinv.
-ring.
-assumption.
-assumption.
-apply Rinv_0_lt_compat; assumption.
-rewrite (Rmult_comm x); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
-ring.
-red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
-apply Rmult_lt_reg_l with (exp eps).
-apply exp_pos.
-rewrite <- exp_plus; rewrite Rmult_1_r; rewrite Rplus_opp_r; rewrite exp_0;
- apply H1.
-rewrite <- exp_0.
-apply exp_increasing; apply Heps.
+  forall y:R, 0 < y -> continue_in ln (fun x:R => 0 < x) y.
+Proof.
+  intros y H.
+  unfold continue_in, limit1_in, limit_in in |- *; intros eps Heps.
+  cut (1 < exp eps); [ intros H1 | idtac ].
+  cut (exp (- eps) < 1); [ intros H2 | idtac ].
+  exists (Rmin (y * (exp eps - 1)) (y * (1 - exp (- eps)))); split.
+  red in |- *; apply P_Rmin.
+  apply Rmult_lt_0_compat.
+  assumption.
+  apply Rplus_lt_reg_r with 1.
+  rewrite Rplus_0_r; replace (1 + (exp eps - 1)) with (exp eps);
+    [ apply H1 | ring ].
+  apply Rmult_lt_0_compat.
+  assumption.
+  apply Rplus_lt_reg_r with (exp (- eps)).
+  rewrite Rplus_0_r; replace (exp (- eps) + (1 - exp (- eps))) with 1;
+    [ apply H2 | ring ].
+  unfold dist, R_met, R_dist in |- *; simpl in |- *.
+  intros x [[H3 H4] H5].
+  cut (y * (x * / y) = x).
+  intro Hxyy. 
+  replace (ln x - ln y) with (ln (x * / y)).
+  case (Rtotal_order x y); [ intros Hxy | intros [Hxy| Hxy] ].
+  rewrite Rabs_left.
+  apply Ropp_lt_cancel; rewrite Ropp_involutive.
+  apply exp_lt_inv.
+  rewrite exp_ln.
+  apply Rmult_lt_reg_l with (r := y).
+  apply H.
+  rewrite Hxyy.
+  apply Ropp_lt_cancel.
+  apply Rplus_lt_reg_r with (r := y).
+  replace (y + - (y * exp (- eps))) with (y * (1 - exp (- eps)));
+  [ idtac | ring ].
+  replace (y + - x) with (Rabs (x - y)).
+  apply Rlt_le_trans with (1 := H5); apply Rmin_r.
+  rewrite Rabs_left; [ ring | idtac ].
+  apply (Rlt_minus _ _ Hxy).
+  apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
+  rewrite <- ln_1.
+  apply ln_increasing.
+  apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
+  apply Rmult_lt_reg_l with (r := y).
+  apply H.
+  rewrite Hxyy; rewrite Rmult_1_r; apply Hxy.
+  rewrite Hxy; rewrite Rinv_r.
+  rewrite ln_1; rewrite Rabs_R0; apply Heps.
+  red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
+  rewrite Rabs_right.
+  apply exp_lt_inv.
+  rewrite exp_ln.
+  apply Rmult_lt_reg_l with (r := y).
+  apply H.
+  rewrite Hxyy.
+  apply Rplus_lt_reg_r with (r := - y).
+  replace (- y + y * exp eps) with (y * (exp eps - 1)); [ idtac | ring ].
+  replace (- y + x) with (Rabs (x - y)).
+  apply Rlt_le_trans with (1 := H5); apply Rmin_l.
+  rewrite Rabs_right; [ ring | idtac ].
+  left; apply (Rgt_minus _ _ Hxy).
+  apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
+  rewrite <- ln_1.
+  apply Rgt_ge; red in |- *; apply ln_increasing.
+  apply Rlt_0_1.
+  apply Rmult_lt_reg_l with (r := y).
+  apply H.
+  rewrite Hxyy; rewrite Rmult_1_r; apply Hxy.
+  rewrite ln_mult.
+  rewrite ln_Rinv.
+  ring.
+  assumption.
+  assumption.
+  apply Rinv_0_lt_compat; assumption.
+  rewrite (Rmult_comm x); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
+  ring.
+  red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
+  apply Rmult_lt_reg_l with (exp eps).
+  apply exp_pos.
+  rewrite <- exp_plus; rewrite Rmult_1_r; rewrite Rplus_opp_r; rewrite exp_0;
+    apply H1.
+  rewrite <- exp_0.
+  apply exp_increasing; apply Heps.
 Qed.
 
 (******************************************************************)
-(*                        Definition of  Rpower                   *)
+(** *                     Definition of  Rpower                   *)
 (******************************************************************)
- 
+
 Definition Rpower (x y:R) := exp (y * ln x).
 
 Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
 
 (******************************************************************)
-(*                        Properties of  Rpower                   *)
+(** *                     Properties of  Rpower                   *)
 (******************************************************************)
- 
+
 Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y.
-intros x y z; unfold Rpower in |- *.
-rewrite Rmult_plus_distr_r; rewrite exp_plus; auto.
+Proof.
+  intros x y z; unfold Rpower in |- *.
+  rewrite Rmult_plus_distr_r; rewrite exp_plus; auto.
 Qed.
- 
+
 Theorem Rpower_mult : forall x y z:R, (x ^R y) ^R z = x ^R (y * z).
-intros x y z; unfold Rpower in |- *.
-rewrite ln_exp.
-replace (z * (y * ln x)) with (y * z * ln x).
-reflexivity.
-ring.
+Proof.
+  intros x y z; unfold Rpower in |- *.
+  rewrite ln_exp.
+  replace (z * (y * ln x)) with (y * z * ln x).
+  reflexivity.
+  ring.
 Qed.
- 
+
 Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1.
-intros x H; unfold Rpower in |- *.
-rewrite Rmult_0_l; apply exp_0.
+Proof.
+  intros x H; unfold Rpower in |- *.
+  rewrite Rmult_0_l; apply exp_0.
 Qed.
- 
+
 Theorem Rpower_1 : forall x:R, 0 < x -> x ^R 1 = x.
-intros x H; unfold Rpower in |- *.
-rewrite Rmult_1_l; apply exp_ln; apply H.
+Proof.
+  intros x H; unfold Rpower in |- *.
+  rewrite Rmult_1_l; apply exp_ln; apply H.
 Qed.
- 
+
 Theorem Rpower_pow : forall (n:nat) (x:R), 0 < x -> x ^R INR n = x ^ n.
-intros n; elim n; simpl in |- *; auto; fold INR in |- *.
-intros x H; apply Rpower_O; auto.
-intros n1; case n1.
-intros H x H0; simpl in |- *; rewrite Rmult_1_r; apply Rpower_1; auto.
-intros n0 H x H0; rewrite Rpower_plus; rewrite H; try rewrite Rpower_1;
- try apply Rmult_comm || assumption.
-Qed.
- 
+Proof.
+  intros n; elim n; simpl in |- *; auto; fold INR in |- *.
+  intros x H; apply Rpower_O; auto.
+  intros n1; case n1.
+  intros H x H0; simpl in |- *; rewrite Rmult_1_r; apply Rpower_1; auto.
+  intros n0 H x H0; rewrite Rpower_plus; rewrite H; try rewrite Rpower_1;
+    try apply Rmult_comm || assumption.
+Qed.
+
 Theorem Rpower_lt :
- forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z.
-intros x y z H H0 H1.
-unfold Rpower in |- *.
-apply exp_increasing.
-apply Rmult_lt_compat_r.
-rewrite <- ln_1; apply ln_increasing.
-apply Rlt_0_1.
-apply H.
-apply H1.
-Qed.
- 
+  forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z.
+Proof.
+  intros x y z H H0 H1.
+  unfold Rpower in |- *.
+  apply exp_increasing.
+  apply Rmult_lt_compat_r.
+  rewrite <- ln_1; apply ln_increasing.
+  apply Rlt_0_1.
+  apply H.
+  apply H1.
+Qed.
+
 Theorem Rpower_sqrt : forall x:R, 0 < x -> x ^R (/ 2) = sqrt x.
-intros x H.
-apply ln_inv.
-unfold Rpower in |- *; apply exp_pos.
-apply sqrt_lt_R0; apply H.
-apply Rmult_eq_reg_l with (INR 2).
-apply exp_inv.
-fold Rpower in |- *.
-cut ((x ^R (/ 2)) ^R INR 2 = sqrt x ^R INR 2).
-unfold Rpower in |- *; auto.
-rewrite Rpower_mult.
-rewrite Rinv_l.
-replace 1 with (INR 1); auto.
-repeat rewrite Rpower_pow; simpl in |- *.
-pattern x at 1 in |- *; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)).
-ring.
-apply sqrt_lt_R0; apply H.
-apply H.
-apply not_O_INR; discriminate.
-apply not_O_INR; discriminate.
-Qed.
- 
+Proof.
+  intros x H.
+  apply ln_inv.
+  unfold Rpower in |- *; apply exp_pos.
+  apply sqrt_lt_R0; apply H.
+  apply Rmult_eq_reg_l with (INR 2).
+  apply exp_inv.
+  fold Rpower in |- *.
+  cut ((x ^R (/ 2)) ^R INR 2 = sqrt x ^R INR 2).
+  unfold Rpower in |- *; auto.
+  rewrite Rpower_mult.
+  rewrite Rinv_l.
+  replace 1 with (INR 1); auto.
+  repeat rewrite Rpower_pow; simpl in |- *.
+  pattern x at 1 in |- *; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)).
+  ring.
+  apply sqrt_lt_R0; apply H.
+  apply H.
+  apply not_O_INR; discriminate.
+  apply not_O_INR; discriminate.
+Qed.
+
 Theorem Rpower_Ropp : forall x y:R, x ^R (- y) = / x ^R y.
-unfold Rpower in |- *.
-intros x y; rewrite Ropp_mult_distr_l_reverse.
-apply exp_Ropp.
+Proof.
+  unfold Rpower in |- *.
+  intros x y; rewrite Ropp_mult_distr_l_reverse.
+  apply exp_Ropp.
 Qed.
- 
+
 Theorem Rle_Rpower :
- forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m.
-intros e n m H H0 H1; case H1.
-intros H2; left; apply Rpower_lt; assumption.
-intros H2; rewrite H2; right; reflexivity.
+  forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m.
+Proof.
+  intros e n m H H0 H1; case H1.
+  intros H2; left; apply Rpower_lt; assumption.
+  intros H2; rewrite H2; right; reflexivity.
 Qed.
-  
+
 Theorem ln_lt_2 : / 2 < ln 2.
-apply Rmult_lt_reg_l with (r := 2).
-prove_sup0.
-rewrite Rinv_r.
-apply exp_lt_inv.
-apply Rle_lt_trans with (1 := exp_le_3).
-change (3 < 2 ^R 2) in |- *.
-repeat rewrite Rpower_plus; repeat rewrite Rpower_1.
-repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
- repeat rewrite Rmult_1_l.
-pattern 3 at 1 in |- *; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1);
- [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ].
-prove_sup0.
-discrR.
-Qed.
-
-(**************************************)
-(* Differentiability of Ln and Rpower *)
-(**************************************)
+Proof.
+  apply Rmult_lt_reg_l with (r := 2).
+  prove_sup0.
+  rewrite Rinv_r.
+  apply exp_lt_inv.
+  apply Rle_lt_trans with (1 := exp_le_3).
+  change (3 < 2 ^R 2) in |- *.
+  repeat rewrite Rpower_plus; repeat rewrite Rpower_1.
+  repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
+    repeat rewrite Rmult_1_l.
+  pattern 3 at 1 in |- *; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1);
+    [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ].
+  prove_sup0.
+  discrR.
+Qed.
+
+(*****************************************)
+(** * Differentiability of Ln and Rpower *)
+(*****************************************)
 
 Theorem limit1_ext :
- forall (f g:R -> R) (D:R -> Prop) (l x:R),
-   (forall x:R, D x -> f x = g x) -> limit1_in f D l x -> limit1_in g D l x.
-intros f g D l x H; unfold limit1_in, limit_in in |- *.
-intros H0 eps H1; case (H0 eps); auto.
-intros x0 [H2 H3]; exists x0; split; auto.
-intros x1 [H4 H5]; rewrite <- H; auto.
+  forall (f g:R -> R) (D:R -> Prop) (l x:R),
+    (forall x:R, D x -> f x = g x) -> limit1_in f D l x -> limit1_in g D l x.
+Proof.
+  intros f g D l x H; unfold limit1_in, limit_in in |- *.
+  intros H0 eps H1; case (H0 eps); auto.
+  intros x0 [H2 H3]; exists x0; split; auto.
+  intros x1 [H4 H5]; rewrite <- H; auto.
 Qed.
 
 Theorem limit1_imp :
- forall (f:R -> R) (D D1:R -> Prop) (l x:R),
-   (forall x:R, D1 x -> D x) -> limit1_in f D l x -> limit1_in f D1 l x.
-intros f D D1 l x H; unfold limit1_in, limit_in in |- *.
-intros H0 eps H1; case (H0 eps H1); auto.
-intros alpha [H2 H3]; exists alpha; split; auto.
-intros d [H4 H5]; apply H3; split; auto.
+  forall (f:R -> R) (D D1:R -> Prop) (l x:R),
+    (forall x:R, D1 x -> D x) -> limit1_in f D l x -> limit1_in f D1 l x.
+Proof.
+  intros f D D1 l x H; unfold limit1_in, limit_in in |- *.
+  intros H0 eps H1; case (H0 eps H1); auto.
+  intros alpha [H2 H3]; exists alpha; split; auto.
+  intros d [H4 H5]; apply H3; split; auto.
 Qed.
 
 Theorem Rinv_Rdiv : forall x y:R, x <> 0 -> y <> 0 -> / (x / y) = y / x.
-intros x y H1 H2; unfold Rdiv in |- *; rewrite Rinv_mult_distr.
-rewrite Rinv_involutive.
-apply Rmult_comm.
-assumption.
-assumption.
-apply Rinv_neq_0_compat; assumption.
+Proof.
+  intros x y H1 H2; unfold Rdiv in |- *; rewrite Rinv_mult_distr.
+  rewrite Rinv_involutive.
+  apply Rmult_comm.
+  assumption.
+  assumption.
+  apply Rinv_neq_0_compat; assumption.
 Qed.
 
 Theorem Dln : forall y:R, 0 < y -> D_in ln Rinv (fun x:R => 0 < x) y.
-intros y Hy; unfold D_in in |- *.
-apply limit1_ext with
- (f := fun x:R => / ((exp (ln x) - exp (ln y)) / (ln x - ln y))).
-intros x [HD1 HD2]; repeat rewrite exp_ln.
-unfold Rdiv in |- *; rewrite Rinv_mult_distr.
-rewrite Rinv_involutive.
-apply Rmult_comm.
-apply Rminus_eq_contra.
-red in |- *; intros H2; case HD2.
-symmetry  in |- *; apply (ln_inv _ _ HD1 Hy H2).
-apply Rminus_eq_contra; apply (sym_not_eq HD2).
-apply Rinv_neq_0_compat; apply Rminus_eq_contra; red in |- *; intros H2;
- case HD2; apply ln_inv; auto.
-assumption.
-assumption.
-apply limit_inv with
- (f := fun x:R => (exp (ln x) - exp (ln y)) / (ln x - ln y)).
-apply limit1_imp with
- (f := fun x:R => (fun x:R => (exp x - exp (ln y)) / (x - ln y)) (ln x))
- (D := Dgf (D_x (fun x:R => 0 < x) y) (D_x (fun x:R => True) (ln y)) ln).
-intros x [H1 H2]; split.
-split; auto.
-split; auto.
-red in |- *; intros H3; case H2; apply ln_inv; auto.
-apply limit_comp with
- (l := ln y) (g := fun x:R => (exp x - exp (ln y)) / (x - ln y)) (f := ln).
-apply ln_continue; auto.
-assert (H0 := derivable_pt_lim_exp (ln y)); unfold derivable_pt_lim in H0;
- unfold limit1_in in |- *; unfold limit_in in |- *; 
- simpl in |- *; unfold R_dist in |- *; intros; elim (H0 _ H); 
- intros; exists (pos x); split.
-apply (cond_pos x).
-intros; pattern y at 3 in |- *; rewrite <- exp_ln.
-pattern x0 at 1 in |- *; replace x0 with (ln y + (x0 - ln y));
- [ idtac | ring ].
-apply H1.
-elim H2; intros H3 _; unfold D_x in H3; elim H3; clear H3; intros _ H3;
- apply Rminus_eq_contra; apply (sym_not_eq (A:=R)); 
- apply H3.
-elim H2; clear H2; intros _ H2; apply H2.
-assumption.
-red in |- *; intro; rewrite H in Hy; elim (Rlt_irrefl _ Hy).
+Proof.
+  intros y Hy; unfold D_in in |- *.
+  apply limit1_ext with
+    (f := fun x:R => / ((exp (ln x) - exp (ln y)) / (ln x - ln y))).
+  intros x [HD1 HD2]; repeat rewrite exp_ln.
+  unfold Rdiv in |- *; rewrite Rinv_mult_distr.
+  rewrite Rinv_involutive.
+  apply Rmult_comm.
+  apply Rminus_eq_contra.
+  red in |- *; intros H2; case HD2.
+  symmetry  in |- *; apply (ln_inv _ _ HD1 Hy H2).
+  apply Rminus_eq_contra; apply (sym_not_eq HD2).
+  apply Rinv_neq_0_compat; apply Rminus_eq_contra; red in |- *; intros H2;
+    case HD2; apply ln_inv; auto.
+  assumption.
+  assumption.
+  apply limit_inv with
+    (f := fun x:R => (exp (ln x) - exp (ln y)) / (ln x - ln y)).
+  apply limit1_imp with
+    (f := fun x:R => (fun x:R => (exp x - exp (ln y)) / (x - ln y)) (ln x))
+    (D := Dgf (D_x (fun x:R => 0 < x) y) (D_x (fun x:R => True) (ln y)) ln).
+  intros x [H1 H2]; split.
+  split; auto.
+  split; auto.
+  red in |- *; intros H3; case H2; apply ln_inv; auto.
+  apply limit_comp with
+    (l := ln y) (g := fun x:R => (exp x - exp (ln y)) / (x - ln y)) (f := ln).
+  apply ln_continue; auto.
+  assert (H0 := derivable_pt_lim_exp (ln y)); unfold derivable_pt_lim in H0;
+    unfold limit1_in in |- *; unfold limit_in in |- *; 
+      simpl in |- *; unfold R_dist in |- *; intros; elim (H0 _ H); 
+        intros; exists (pos x); split.
+  apply (cond_pos x).
+  intros; pattern y at 3 in |- *; rewrite <- exp_ln.
+  pattern x0 at 1 in |- *; replace x0 with (ln y + (x0 - ln y));
+    [ idtac | ring ].
+  apply H1.
+  elim H2; intros H3 _; unfold D_x in H3; elim H3; clear H3; intros _ H3;
+    apply Rminus_eq_contra; apply (sym_not_eq (A:=R)); 
+      apply H3.
+  elim H2; clear H2; intros _ H2; apply H2.
+  assumption.
+  red in |- *; intro; rewrite H in Hy; elim (Rlt_irrefl _ Hy).
 Qed.
 
 Lemma derivable_pt_lim_ln : forall x:R, 0 < x -> derivable_pt_lim ln x (/ x).
-intros; assert (H0 := Dln x H); unfold D_in in H0; unfold limit1_in in H0;
- unfold limit_in in H0; simpl in H0; unfold R_dist in H0;
- unfold derivable_pt_lim in |- *; intros; elim (H0 _ H1); 
- intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2));
- assert (H4 : 0 < alp).
-unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec x0 (x / 2)); intro.
-apply H2.
-unfold Rdiv in |- *; apply Rmult_lt_0_compat;
- [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
-exists (mkposreal _ H4); intros; pattern h at 2 in |- *;
- replace h with (x + h - x); [ idtac | ring ].
-apply H3; split.
-unfold D_x in |- *; split.
-case (Rcase_abs h); intro.
-assert (H7 : Rabs h < x / 2).
-apply Rlt_le_trans with alp.
-apply H6.
-unfold alp in |- *; apply Rmin_r.
-apply Rlt_trans with (x / 2).
-unfold Rdiv in |- *; apply Rmult_lt_0_compat;
- [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
-rewrite Rabs_left in H7.
-apply Rplus_lt_reg_r with (- h - x / 2).
-replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ].
-pattern x at 2 in |- *; rewrite double_var.
-replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ].
-apply r.
-apply Rplus_lt_le_0_compat; [ assumption | apply Rge_le; apply r ].
-apply (sym_not_eq (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h;
- [ apply H5 | ring ].
-replace (x + h - x) with h;
- [ apply Rlt_le_trans with alp;
+Proof.
+  intros; assert (H0 := Dln x H); unfold D_in in H0; unfold limit1_in in H0;
+    unfold limit_in in H0; simpl in H0; unfold R_dist in H0;
+      unfold derivable_pt_lim in |- *; intros; elim (H0 _ H1); 
+        intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2));
+          assert (H4 : 0 < alp).
+  unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec x0 (x / 2)); intro.
+  apply H2.
+  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
+  exists (mkposreal _ H4); intros; pattern h at 2 in |- *;
+    replace h with (x + h - x); [ idtac | ring ].
+  apply H3; split.
+  unfold D_x in |- *; split.
+  case (Rcase_abs h); intro.
+  assert (H7 : Rabs h < x / 2).
+  apply Rlt_le_trans with alp.
+  apply H6.
+  unfold alp in |- *; apply Rmin_r.
+  apply Rlt_trans with (x / 2).
+  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
+  rewrite Rabs_left in H7.
+  apply Rplus_lt_reg_r with (- h - x / 2).
+  replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ].
+  pattern x at 2 in |- *; rewrite double_var.
+  replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ].
+  apply r.
+  apply Rplus_lt_le_0_compat; [ assumption | apply Rge_le; apply r ].
+  apply (sym_not_eq (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h;
+    [ apply H5 | ring ].
+  replace (x + h - x) with h;
+  [ apply Rlt_le_trans with alp;
     [ apply H6 | unfold alp in |- *; apply Rmin_l ]
- | ring ].
+    | ring ].
 Qed.
 
 Theorem D_in_imp :
- forall (f g:R -> R) (D D1:R -> Prop) (x:R),
-   (forall x:R, D1 x -> D x) -> D_in f g D x -> D_in f g D1 x.
-intros f g D D1 x H; unfold D_in in |- *.
-intros H0; apply limit1_imp with (D := D_x D x); auto.
-intros x1 [H1 H2]; split; auto.
+  forall (f g:R -> R) (D D1:R -> Prop) (x:R),
+    (forall x:R, D1 x -> D x) -> D_in f g D x -> D_in f g D1 x.
+Proof.
+  intros f g D D1 x H; unfold D_in in |- *.
+  intros H0; apply limit1_imp with (D := D_x D x); auto.
+  intros x1 [H1 H2]; split; auto.
 Qed.
 
 Theorem D_in_ext :
- forall (f g h:R -> R) (D:R -> Prop) (x:R),
-   f x = g x -> D_in h f D x -> D_in h g D x.
-intros f g h D x H; unfold D_in in |- *.
-rewrite H; auto.
+  forall (f g h:R -> R) (D:R -> Prop) (x:R),
+    f x = g x -> D_in h f D x -> D_in h g D x.
+Proof.
+  intros f g h D x H; unfold D_in in |- *.
+  rewrite H; auto.
 Qed.
 
 Theorem Dpower :
- forall y z:R,
-   0 < y ->
-   D_in (fun x:R => x ^R z) (fun x:R => z * x ^R (z - 1)) (
-     fun x:R => 0 < x) y.
-intros y z H;
- apply D_in_imp with (D := Dgf (fun x:R => 0 < x) (fun x:R => True) ln).
-intros x H0; repeat split.
-assumption.
-apply D_in_ext with (f := fun x:R => / x * (z * exp (z * ln x))).
-unfold Rminus in |- *; rewrite Rpower_plus; rewrite Rpower_Ropp;
- rewrite (Rpower_1 _ H); ring.
-apply Dcomp with
- (f := ln)
- (g := fun x:R => exp (z * x))
- (df := Rinv)
- (dg := fun x:R => z * exp (z * x)).
-apply (Dln _ H).
-apply D_in_imp with
- (D := Dgf (fun x:R => True) (fun x:R => True) (fun x:R => z * x)).
-intros x H1; repeat split; auto.
-apply
- (Dcomp (fun _:R => True) (fun _:R => True) (fun x => z) exp
-    (fun x:R => z * x) exp); simpl in |- *.
-apply D_in_ext with (f := fun x:R => z * 1).
-apply Rmult_1_r.
-apply (Dmult_const (fun x => True) (fun x => x) (fun x => 1)); apply Dx.
-assert (H0 := derivable_pt_lim_D_in exp exp (z * ln y)); elim H0; clear H0;
- intros _ H0; apply H0; apply derivable_pt_lim_exp.
+  forall y z:R,
+    0 < y ->
+    D_in (fun x:R => x ^R z) (fun x:R => z * x ^R (z - 1)) (
+      fun x:R => 0 < x) y.
+Proof.
+  intros y z H;
+    apply D_in_imp with (D := Dgf (fun x:R => 0 < x) (fun x:R => True) ln).
+  intros x H0; repeat split.
+  assumption.
+  apply D_in_ext with (f := fun x:R => / x * (z * exp (z * ln x))).
+  unfold Rminus in |- *; rewrite Rpower_plus; rewrite Rpower_Ropp;
+    rewrite (Rpower_1 _ H); unfold Rpower; ring.
+  apply Dcomp with
+    (f := ln)
+    (g := fun x:R => exp (z * x))
+    (df := Rinv)
+    (dg := fun x:R => z * exp (z * x)).
+  apply (Dln _ H).
+  apply D_in_imp with
+    (D := Dgf (fun x:R => True) (fun x:R => True) (fun x:R => z * x)).
+  intros x H1; repeat split; auto.
+  apply
+    (Dcomp (fun _:R => True) (fun _:R => True) (fun x => z) exp
+      (fun x:R => z * x) exp); simpl in |- *.
+  apply D_in_ext with (f := fun x:R => z * 1).
+  apply Rmult_1_r.
+  apply (Dmult_const (fun x => True) (fun x => x) (fun x => 1)); apply Dx.
+  assert (H0 := derivable_pt_lim_D_in exp exp (z * ln y)); elim H0; clear H0;
+    intros _ H0; apply H0; apply derivable_pt_lim_exp.
 Qed.
 
 Theorem derivable_pt_lim_power :
- forall x y:R,
-   0 < x -> derivable_pt_lim (fun x => x ^R y) x (y * x ^R (y - 1)).
-intros x y H.
-unfold Rminus in |- *; rewrite Rpower_plus.
-rewrite Rpower_Ropp.
-rewrite Rpower_1; auto.
-rewrite <- Rmult_assoc.
-unfold Rpower in |- *.
-apply derivable_pt_lim_comp with (f1 := ln) (f2 := fun x => exp (y * x)).
-apply derivable_pt_lim_ln; assumption.
-rewrite (Rmult_comm y).
-apply derivable_pt_lim_comp with (f1 := fun x => y * x) (f2 := exp).
-pattern y at 2 in |- *; replace y with (0 * ln x + y * 1).
-apply derivable_pt_lim_mult with (f1 := fun x:R => y) (f2 := fun x:R => x).
-apply derivable_pt_lim_const with (a := y).
-apply derivable_pt_lim_id.
-ring.
-apply derivable_pt_lim_exp.
+  forall x y:R,
+    0 < x -> derivable_pt_lim (fun x => x ^R y) x (y * x ^R (y - 1)).
+Proof.
+  intros x y H.
+  unfold Rminus in |- *; rewrite Rpower_plus.
+  rewrite Rpower_Ropp.
+  rewrite Rpower_1; auto.
+  rewrite <- Rmult_assoc.
+  unfold Rpower in |- *.
+  apply derivable_pt_lim_comp with (f1 := ln) (f2 := fun x => exp (y * x)).
+  apply derivable_pt_lim_ln; assumption.
+  rewrite (Rmult_comm y).
+  apply derivable_pt_lim_comp with (f1 := fun x => y * x) (f2 := exp).
+  pattern y at 2 in |- *; replace y with (0 * ln x + y * 1).
+  apply derivable_pt_lim_mult with (f1 := fun x:R => y) (f2 := fun x:R => x).
+  apply derivable_pt_lim_const with (a := y).
+  apply derivable_pt_lim_id.
+  ring.
+  apply derivable_pt_lim_exp.
 Qed.