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, 617 insertions, 656 deletions

diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index b283b9fd8..30b4a5396 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -16,16 +16,15 @@
 (*                                                      *)
 (********************************************************)
 
-Require Rbase.
+Require Import Rbase.
 Require Export R_Ifp.
 Require Export Rbasic_fun.
 Require Export R_sqr.
 Require Export SplitAbsolu.
 Require Export SplitRmult.
 Require Export ArithProp.
-Require Omega.
-Require Zpower.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Omega.
+Require Import Zpower.
 Open Local Scope nat_scope.
 Open Local Scope R_scope.
 
@@ -33,522 +32,491 @@ Open Local Scope R_scope.
 (**  Lemmas about factorial    *)
 (*******************************)
 (*********)
-Lemma INR_fact_neq_0:(n:nat)~(INR (fact n))==R0.
+Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0.
 Proof.
-Intro;Red;Intro;Apply (not_O_INR (fact n) (fact_neq_0 n));Assumption.
+intro; red in |- *; intro; apply (not_O_INR (fact n) (fact_neq_0 n));
+ assumption.
 Qed.    
 
 (*********)
-Lemma fact_simpl : (n:nat) (fact (S n))=(mult (S n) (fact n)).
+Lemma fact_simpl : forall n:nat, fact (S n) = (S n * fact n)%nat.
 Proof.
-Intro; Reflexivity.
+intro; reflexivity.
 Qed. 
 
 (*********)
-Lemma simpl_fact:(n:nat)(Rmult (Rinv (INR (fact (S n)))) 
-         (Rinv (Rinv (INR (fact n)))))==
-         (Rinv (INR (S n))).
+Lemma simpl_fact :
+ forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n).
 Proof.
-Intro;Rewrite (Rinv_Rinv (INR (fact n)) (INR_fact_neq_0 n)); 
- Unfold 1 fact;Cbv Beta Iota;Fold fact;
- Rewrite (mult_INR (S n) (fact n));
- Rewrite (Rinv_Rmult (INR (S n)) (INR (fact n))).
-Rewrite (Rmult_assoc (Rinv (INR (S n))) (Rinv (INR (fact n))) 
-  (INR (fact n)));Rewrite (Rinv_l (INR (fact n)) (INR_fact_neq_0 n));
- Apply (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1).
-Apply not_O_INR;Auto.
-Apply INR_fact_neq_0.
+intro; rewrite (Rinv_involutive (INR (fact n)) (INR_fact_neq_0 n));
+ unfold fact at 1 in |- *; cbv beta iota in |- *; fold fact in |- *;
+ rewrite (mult_INR (S n) (fact n));
+ rewrite (Rinv_mult_distr (INR (S n)) (INR (fact n))).
+rewrite (Rmult_assoc (/ INR (S n)) (/ INR (fact n)) (INR (fact n)));
+ rewrite (Rinv_l (INR (fact n)) (INR_fact_neq_0 n));
+ apply (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1).
+apply not_O_INR; auto.
+apply INR_fact_neq_0.
 Qed.
 
 (*******************************)
 (*          Power              *)
 (*******************************)
 (*********)
-Fixpoint pow [r:R;n:nat]:R:=
-  Cases n of
-     O     => R1
-    |(S n) => (Rmult r (pow r n))
+Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+  match n with
+  | O => 1
+  | S n => r * pow r n
   end.
 
-Infix "^" pow (at level 2, left associativity) : R_scope V8only.
+Infix "^" := pow : R_scope.
 
-Lemma pow_O: (x : R)  (pow x O) == R1.
+Lemma pow_O : forall x:R, x ^ 0 = 1.
 Proof.
-Reflexivity.
+reflexivity.
 Qed.
  
-Lemma pow_1: (x : R)  (pow x (1)) == x.
+Lemma pow_1 : forall x:R, x ^ 1 = x.
 Proof.
-Simpl; Auto with real.
+simpl in |- *; auto with real.
 Qed.
  
-Lemma pow_add:
- (x : R) (n, m : nat)  (pow x (plus n m)) == (Rmult (pow x n) (pow x m)).
+Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m.
 Proof.
-Intros x n; Elim n; Simpl; Auto with real.
-Intros n0 H' m; Rewrite H'; Auto with real.
+intros x n; elim n; simpl in |- *; auto with real.
+intros n0 H' m; rewrite H'; auto with real.
 Qed.
 
-Lemma pow_nonzero:
-  (x:R) (n:nat) ~(x==R0) -> ~((pow x n)==R0).
+Lemma pow_nonzero : forall (x:R) (n:nat), x <> 0 -> x ^ n <> 0.
 Proof.
-Intro; Induction n; Simpl.
-Intro; Red;Intro;Apply R1_neq_R0;Assumption.
-Intros;Red; Intro;Elim (without_div_Od x (pow x n0) H1).
-Intro; Auto.
-Apply H;Assumption.
+intro; simple induction n; simpl in |- *.
+intro; red in |- *; intro; apply R1_neq_R0; assumption.
+intros; red in |- *; intro; elim (Rmult_integral x (x ^ n0) H1).
+intro; auto.
+apply H; assumption.
 Qed.
 
-Hints Resolve pow_O pow_1 pow_add pow_nonzero:real.
+Hint Resolve pow_O pow_1 pow_add pow_nonzero: real.
  
-Lemma pow_RN_plus:
- (x : R)
- (n, m : nat)
- ~ x == R0 ->  (pow x n) == (Rmult (pow x (plus n m)) (Rinv (pow x m))).
-Proof.
-Intros x n; Elim n; Simpl; Auto with real.
-Intros n0 H' m H'0.
-Rewrite Rmult_assoc; Rewrite <- H'; Auto.
-Qed.
-
-Lemma pow_lt: (x : R) (n : nat) (Rlt R0 x) ->  (Rlt R0 (pow x n)).
-Proof.
-Intros x n; Elim n; Simpl; Auto with real.
-Intros n0 H' H'0; Replace R0 with (Rmult x R0); Auto with real.
-Qed.
-Hints Resolve pow_lt :real.
-
-Lemma Rlt_pow_R1:
- (x : R) (n : nat) (Rlt R1 x) -> (lt O n) ->  (Rlt R1 (pow x n)).
-Proof.
-Intros x n; Elim n; Simpl; Auto with real.
-Intros H' H'0; ElimType False; Omega.
-Intros n0; Case n0.
-Simpl; Rewrite Rmult_1r; Auto.
-Intros n1 H' H'0 H'1.
-Replace R1 with (Rmult R1 R1); Auto with real.
-Apply Rlt_trans with r2 := (Rmult x R1); Auto with real.
-Apply Rlt_monotony; Auto with real.
-Apply Rlt_trans with r2 := R1; Auto with real.
-Apply H'; Auto with arith.
-Qed.
-Hints Resolve Rlt_pow_R1 :real.
-
-Lemma Rlt_pow:
- (x : R) (n, m : nat) (Rlt R1 x) -> (lt n m) ->  (Rlt (pow x n) (pow x m)).
-Proof.
-Intros x n m H' H'0; Replace m with (plus (minus m n) n).
-Rewrite pow_add.
-Pattern 1 (pow x n); Replace (pow x n) with (Rmult R1 (pow x n)); 
- Auto with real.
-Apply Rminus_lt.
-Repeat Rewrite [y : R]  (Rmult_sym y (pow x n)); Rewrite <- Rminus_distr.
-Replace R0 with (Rmult (pow x n) R0); Auto with real.
-Apply Rlt_monotony; Auto with real.
-Apply pow_lt; Auto with real.
-Apply Rlt_trans with r2 := R1; Auto with real.
-Apply Rlt_minus; Auto with real.
-Apply Rlt_pow_R1; Auto with arith.
-Apply simpl_lt_plus_l with p := n; Auto with arith.
-Rewrite le_plus_minus_r; Auto with arith; Rewrite <- plus_n_O; Auto.
-Rewrite plus_sym; Auto with arith.
-Qed.
-Hints Resolve Rlt_pow :real.
+Lemma pow_RN_plus :
+ forall (x:R) (n m:nat), x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m.
+Proof.
+intros x n; elim n; simpl in |- *; auto with real.
+intros n0 H' m H'0.
+rewrite Rmult_assoc; rewrite <- H'; auto.
+Qed.
+
+Lemma pow_lt : forall (x:R) (n:nat), 0 < x -> 0 < x ^ n.
+Proof.
+intros x n; elim n; simpl in |- *; auto with real.
+intros n0 H' H'0; replace 0 with (x * 0); auto with real.
+Qed.
+Hint Resolve pow_lt: real.
+
+Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
+Proof.
+intros x n; elim n; simpl in |- *; auto with real.
+intros H' H'0; elimtype False; omega.
+intros n0; case n0.
+simpl in |- *; rewrite Rmult_1_r; auto.
+intros n1 H' H'0 H'1.
+replace 1 with (1 * 1); auto with real.
+apply Rlt_trans with (r2 := x * 1); auto with real.
+apply Rmult_lt_compat_l; auto with real.
+apply Rlt_trans with (r2 := 1); auto with real.
+apply H'; auto with arith.
+Qed.
+Hint Resolve Rlt_pow_R1: real.
+
+Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.
+Proof.
+intros x n m H' H'0; replace m with (m - n + n)%nat.
+rewrite pow_add.
+pattern (x ^ n) at 1 in |- *; replace (x ^ n) with (1 * x ^ n);
+ auto with real.
+apply Rminus_lt.
+repeat rewrite (fun y:R => Rmult_comm y (x ^ n));
+ rewrite <- Rmult_minus_distr_l.
+replace 0 with (x ^ n * 0); auto with real.
+apply Rmult_lt_compat_l; auto with real.
+apply pow_lt; auto with real.
+apply Rlt_trans with (r2 := 1); auto with real.
+apply Rlt_minus; auto with real.
+apply Rlt_pow_R1; auto with arith.
+apply plus_lt_reg_l with (p := n); auto with arith.
+rewrite le_plus_minus_r; auto with arith; rewrite <- plus_n_O; auto.
+rewrite plus_comm; auto with arith.
+Qed.
+Hint Resolve Rlt_pow: real.
 
 (*********)
-Lemma tech_pow_Rmult:(x:R)(n:nat)(Rmult x (pow x n))==(pow x (S n)).
+Lemma tech_pow_Rmult : forall (x:R) (n:nat), x * x ^ n = x ^ S n.
 Proof.
-Induction n; Simpl; Trivial.
+simple induction n; simpl in |- *; trivial.
 Qed.
 
 (*********)
-Lemma tech_pow_Rplus:(x:R)(a,n:nat)
-  (Rplus (pow x a) (Rmult (INR n) (pow x a)))==
-           (Rmult (INR (S n)) (pow x a)).
-Proof.
-Intros; Pattern 1 (pow x a);  
- Rewrite <-(let (H1,H2)=(Rmult_ne (pow x a)) in H1); 
- Rewrite (Rmult_sym (INR n) (pow x a));
- Rewrite <- (Rmult_Rplus_distr (pow x a) R1 (INR n));
- Rewrite (Rplus_sym R1 (INR n)); Rewrite <-(S_INR n);
- Apply Rmult_sym.
-Qed.
-
-Lemma poly: (n:nat)(x:R)(Rlt R0 x)->
- (Rle (Rplus R1 (Rmult (INR n) x)) (pow  (Rplus R1 x) n)).
-Proof.
-Intros;Elim n.
-Simpl;Cut (Rplus R1 (Rmult R0 x))==R1.
-Intro;Rewrite H0;Unfold Rle;Right; Reflexivity.
-Ring.
-Intros;Unfold pow; Fold pow;
- Apply (Rle_trans (Rplus R1 (Rmult (INR (S n0)) x))
-    (Rmult (Rplus R1 x) (Rplus R1 (Rmult (INR n0) x))) 
-    (Rmult (Rplus R1 x) (pow (Rplus R1 x) n0))).
-Cut (Rmult (Rplus R1 x) (Rplus R1 (Rmult (INR n0) x)))== 
-  (Rplus (Rplus R1 (Rmult (INR (S n0)) x)) 
-         (Rmult (INR n0) (Rmult x x))).
-Intro;Rewrite H1;Pattern 1 (Rplus R1 (Rmult (INR (S n0)) x));
- Rewrite <-(let (H1,H2)=
-   (Rplus_ne (Rplus R1 (Rmult (INR (S n0)) x))) in H1);
- Apply Rle_compatibility;Elim n0;Intros.
-Simpl;Rewrite Rmult_Ol;Unfold Rle;Right;Auto.
-Unfold Rle;Left;Generalize Rmult_gt;Unfold Rgt;Intro;
- Fold (Rsqr x);Apply (H3 (INR (S n1)) (Rsqr x) 
-        (lt_INR_0 (S n1) (lt_O_Sn n1)));Fold (Rgt x R0) in H;
- Apply (pos_Rsqr1 x (imp_not_Req x R0 
-  (or_intror (Rlt x R0) (Rgt x R0) H))).
-Rewrite (S_INR n0);Ring.
-Unfold Rle in H0;Elim H0;Intro. 
-Unfold Rle;Left;Apply Rlt_monotony.
-Rewrite Rplus_sym;
- Apply (Rlt_r_plus_R1 x (Rlt_le R0 x H)).
-Assumption.
-Rewrite H1;Unfold Rle;Right;Trivial.
-Qed.
-
-Lemma Power_monotonic:
- (x:R) (m,n:nat) (Rgt (Rabsolu x) R1) 
-        -> (le m n)
-           -> (Rle (Rabsolu (pow x m)) (Rabsolu (pow x n))).
-Proof.
-Intros x m n H;Induction n;Intros;Inversion H0.
-Unfold Rle; Right; Reflexivity.
-Unfold Rle; Right; Reflexivity.
-Apply (Rle_trans (Rabsolu (pow x m))
-                 (Rabsolu (pow x n))
-                 (Rabsolu (pow x (S n)))).
-Apply Hrecn; Assumption.
-Simpl;Rewrite Rabsolu_mult.
-Pattern 1 (Rabsolu (pow x n)).
-Rewrite <-Rmult_1r.
-Rewrite (Rmult_sym (Rabsolu x) (Rabsolu (pow x n))).
-Apply Rle_monotony.
-Apply Rabsolu_pos.
-Unfold Rgt in H.
-Apply Rlt_le; Assumption.
-Qed.
-
-Lemma Pow_Rabsolu: (x:R) (n:nat)
-     (pow (Rabsolu x) n)==(Rabsolu (pow x n)).
-Proof.
-Intro;Induction n;Simpl.
-Apply sym_eqT;Apply Rabsolu_pos_eq;Apply Rlt_le;Apply Rlt_R0_R1.
-Intros; Rewrite H;Apply sym_eqT;Apply Rabsolu_mult.
-Qed.
-
-
-Lemma Pow_x_infinity:
-  (x:R) (Rgt (Rabsolu x) R1)
-        -> (b:R) (Ex [N:nat] ((n:nat) (ge n N) 
-                     -> (Rge (Rabsolu (pow x n)) b ))).
-Proof.
-Intros;Elim (archimed (Rmult b (Rinv (Rminus (Rabsolu x) R1))));Intros;
-  Clear H1;
-  Cut (Ex[N:nat] (Rge (INR N) (Rmult b (Rinv (Rminus (Rabsolu x) R1))))).
-Intro; Elim H1;Clear H1;Intros;Exists x0;Intros;
- Apply (Rge_trans (Rabsolu (pow x n)) (Rabsolu (pow x x0)) b).
-Apply Rle_sym1;Apply Power_monotonic;Assumption.
-Rewrite <- Pow_Rabsolu;Cut (Rabsolu x)==(Rplus R1 (Rminus (Rabsolu x) R1)).
-Intro; Rewrite H3;
- Apply (Rge_trans (pow (Rplus R1 (Rminus (Rabsolu x) R1)) x0)
-                 (Rplus R1 (Rmult (INR x0)  
-                                  (Rminus (Rabsolu x) R1)))
-                 b).
-Apply Rle_sym1;Apply poly;Fold (Rgt (Rminus (Rabsolu x) R1) R0);
- Apply Rgt_minus;Assumption.
-Apply (Rge_trans 
-         (Rplus R1 (Rmult (INR x0) (Rminus (Rabsolu x) R1)))
-         (Rmult (INR x0) (Rminus (Rabsolu x) R1))
-         b).
-Apply Rle_sym1; Apply Rlt_le;Rewrite (Rplus_sym R1 
-                   (Rmult (INR x0) (Rminus (Rabsolu x) R1)));
- Pattern 1 (Rmult (INR x0) (Rminus (Rabsolu x) R1));
- Rewrite <- (let (H1,H2) = (Rplus_ne 
-            (Rmult (INR x0) (Rminus (Rabsolu x) R1))) in
-         H1);
- Apply Rlt_compatibility;
- Apply Rlt_R0_R1.
-Cut b==(Rmult (Rmult b (Rinv (Rminus (Rabsolu x) R1)))
-              (Rminus (Rabsolu x) R1)).
-Intros; Rewrite H4;Apply Rge_monotony.
-Apply Rge_minus;Unfold Rge; Left; Assumption.
-Assumption.
-Rewrite Rmult_assoc;Rewrite Rinv_l.
-Ring.
-Apply imp_not_Req; Right;Apply Rgt_minus;Assumption.
-Ring.
-Cut `0<= (up (Rmult b (Rinv (Rminus (Rabsolu x) R1))))`\/
-     `(up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))) <=  0`.
-Intros;Elim H1;Intro.
-Elim (IZN (up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))) H2);Intros;Exists x0;
- Apply (Rge_trans 
-   (INR x0)
-   (IZR (up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))))
-   (Rmult b (Rinv (Rminus (Rabsolu x) R1)))).
-Rewrite INR_IZR_INZ;Apply IZR_ge;Omega.
-Unfold Rge; Left; Assumption.
-Exists O;Apply (Rge_trans (INR (0))
-          (IZR (up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))))
-          (Rmult b (Rinv (Rminus (Rabsolu x) R1)))).
-Rewrite INR_IZR_INZ;Apply IZR_ge;Simpl;Omega.
-Unfold Rge; Left; Assumption.
-Omega.
-Qed.
-
-Lemma pow_ne_zero:
-  (n:nat) ~(n=(0))-> (pow R0 n) == R0.
-Proof.
-Induction n.
-Simpl;Auto.
-Intros;Elim H;Reflexivity.
-Intros; Simpl;Apply Rmult_Ol.
-Qed.
-
-Lemma Rinv_pow:
-  (x:R) (n:nat) ~(x==R0) -> (Rinv (pow x n))==(pow (Rinv x) n).
-Proof.
-Intros; Elim n; Simpl.
-Apply Rinv_R1.
-Intro m;Intro;Rewrite Rinv_Rmult.
-Rewrite H0; Reflexivity;Assumption.
-Assumption.
-Apply pow_nonzero;Assumption.
-Qed.
-
-Lemma pow_lt_1_zero:
-  (x:R) (Rlt (Rabsolu x) R1)
-        -> (y:R) (Rlt R0 y) 
-                 -> (Ex[N:nat] (n:nat) (ge n N)
-                         -> (Rlt (Rabsolu (pow x n)) y)).
-Proof.
-Intros;Elim (Req_EM x R0);Intro. 
-Exists (1);Rewrite H1;Intros n GE;Rewrite pow_ne_zero.
-Rewrite Rabsolu_R0;Assumption.
-Inversion GE;Auto.
-Cut (Rgt (Rabsolu (Rinv x)) R1).
-Intros;Elim (Pow_x_infinity (Rinv x) H2 (Rplus (Rinv y) R1));Intros N.
-Exists N;Intros;Rewrite <- (Rinv_Rinv y).
-Rewrite <- (Rinv_Rinv (Rabsolu (pow x n))).
-Apply Rinv_lt.
-Apply Rmult_lt_pos.
-Apply Rlt_Rinv.
-Assumption.
-Apply Rlt_Rinv.
-Apply Rabsolu_pos_lt.
-Apply pow_nonzero.
-Assumption.
-Rewrite <- Rabsolu_Rinv.
-Rewrite Rinv_pow.
-Apply (Rlt_le_trans (Rinv y)
-                    (Rplus (Rinv y) R1)
-                    (Rabsolu (pow (Rinv x) n))).
-Pattern 1 (Rinv y).
-Rewrite <- (let (H1,H2) = 
-                (Rplus_ne (Rinv y)) in H1).
-Apply Rlt_compatibility.
-Apply Rlt_R0_R1.
-Apply Rle_sym2.
-Apply H3.
-Assumption.
-Assumption.
-Apply pow_nonzero.
-Assumption.
-Apply Rabsolu_no_R0.
-Apply pow_nonzero.
-Assumption.
-Apply imp_not_Req.
-Right; Unfold Rgt; Assumption.
-Rewrite <- (Rinv_Rinv R1).
-Rewrite Rabsolu_Rinv.
-Unfold Rgt; Apply Rinv_lt.
-Apply Rmult_lt_pos.
-Apply Rabsolu_pos_lt.
-Assumption.
-Rewrite Rinv_R1; Apply Rlt_R0_R1.
-Rewrite Rinv_R1; Assumption.
-Assumption.
-Red;Intro; Apply R1_neq_R0;Assumption.
-Qed.
-
-Lemma pow_R1:
- (r : R) (n : nat) (pow r n) == R1 ->  (Rabsolu r) == R1 \/ n = O.
-Proof.
-Intros r n H'.
-Case (Req_EM (Rabsolu r) R1); Auto; Intros H'1.
-Case (not_Req ? ? H'1); Intros H'2.
-Generalize H'; Case n; Auto.
-Intros n0 H'0.
-Cut ~ r == R0; [Intros Eq1 | Idtac].
-Cut ~ (Rabsolu r) == R0; [Intros Eq2 | Apply Rabsolu_no_R0]; Auto.
-Absurd (Rlt (pow (Rabsolu (Rinv r)) O) (pow (Rabsolu (Rinv r)) (S n0))); Auto.
-Replace (pow (Rabsolu (Rinv r)) (S n0)) with R1.
-Simpl; Apply Rlt_antirefl; Auto.
-Rewrite Rabsolu_Rinv; Auto.
-Rewrite <- Rinv_pow; Auto.
-Rewrite Pow_Rabsolu; Auto.
-Rewrite H'0; Rewrite Rabsolu_right; Auto with real.
-Apply Rle_ge; Auto with real.
-Apply Rlt_pow; Auto with arith.
-Rewrite Rabsolu_Rinv; Auto.
-Apply Rlt_monotony_contra with z := (Rabsolu r).
-Case (Rabsolu_pos r); Auto.
-Intros H'3; Case Eq2; Auto.
-Rewrite Rmult_1r; Rewrite Rinv_r; Auto with real.
-Red;Intro;Absurd ``(pow r (S n0)) == 1``;Auto.
-Simpl; Rewrite H; Rewrite Rmult_Ol; Auto with real.
-Generalize H'; Case n; Auto.
-Intros n0 H'0.
-Cut ~ r == R0; [Intros Eq1 | Auto with real].
-Cut ~ (Rabsolu r) == R0; [Intros Eq2 | Apply Rabsolu_no_R0]; Auto.
-Absurd (Rlt (pow (Rabsolu r) O) (pow (Rabsolu r) (S n0))); 
-  Auto with real arith.
-Repeat Rewrite Pow_Rabsolu; Rewrite H'0; Simpl; Auto with real.
-Red;Intro;Absurd ``(pow r (S n0)) == 1``;Auto.
-Simpl; Rewrite H; Rewrite Rmult_Ol; Auto with real.
-Qed.
-
-Lemma pow_Rsqr : (x:R;n:nat) (pow x (mult (2) n))==(pow (Rsqr x) n).
-Proof.
-Intros; Induction n.
-Reflexivity.
-Replace (mult (2) (S n)) with (S (S (mult (2) n))).
-Replace (pow x (S (S (mult (2) n)))) with ``x*x*(pow x (mult (S (S O)) n))``.
-Rewrite Hrecn; Reflexivity.
-Simpl; Ring.
-Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
-Qed.
-
-Lemma pow_le : (a:R;n:nat) ``0<=a`` -> ``0<=(pow a n)``.
-Proof.
-Intros; Induction n.
-Simpl; Left; Apply Rlt_R0_R1.
-Simpl; Apply Rmult_le_pos; Assumption.
+Lemma tech_pow_Rplus :
+ forall (x:R) (a n:nat), x ^ a + INR n * x ^ a = INR (S n) * x ^ a.
+Proof.
+intros; pattern (x ^ a) at 1 in |- *;
+ rewrite <- (let (H1, H2) := Rmult_ne (x ^ a) in H1);
+ rewrite (Rmult_comm (INR n) (x ^ a));
+ rewrite <- (Rmult_plus_distr_l (x ^ a) 1 (INR n));
+ rewrite (Rplus_comm 1 (INR n)); rewrite <- (S_INR n); 
+ apply Rmult_comm.
+Qed.
+
+Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.
+Proof.
+intros; elim n.
+simpl in |- *; cut (1 + 0 * x = 1).
+intro; rewrite H0; unfold Rle in |- *; right; reflexivity.
+ring.
+intros; unfold pow in |- *; fold pow in |- *;
+ apply
+  (Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x))
+     ((1 + x) * (1 + x) ^ n0)).
+cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)).
+intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1 in |- *;
+ rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1);
+ apply Rplus_le_compat_l; elim n0; intros.
+simpl in |- *; rewrite Rmult_0_l; unfold Rle in |- *; right; auto.
+unfold Rle in |- *; left; generalize Rmult_gt_0_compat; unfold Rgt in |- *;
+ intro; fold (Rsqr x) in |- *;
+ apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (lt_O_Sn n1)));
+ fold (x > 0) in H;
+ apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))).
+rewrite (S_INR n0); ring.
+unfold Rle in H0; elim H0; intro. 
+unfold Rle in |- *; left; apply Rmult_lt_compat_l.
+rewrite Rplus_comm; apply (Rle_lt_0_plus_1 x (Rlt_le 0 x H)).
+assumption.
+rewrite H1; unfold Rle in |- *; right; trivial.
+Qed.
+
+Lemma Power_monotonic :
+ forall (x:R) (m n:nat),
+   Rabs x > 1 -> (m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n).
+Proof.
+intros x m n H; induction  n as [| n Hrecn]; intros; inversion H0.
+unfold Rle in |- *; right; reflexivity.
+unfold Rle in |- *; right; reflexivity.
+apply (Rle_trans (Rabs (x ^ m)) (Rabs (x ^ n)) (Rabs (x ^ S n))).
+apply Hrecn; assumption.
+simpl in |- *; rewrite Rabs_mult.
+pattern (Rabs (x ^ n)) at 1 in |- *.
+rewrite <- Rmult_1_r.
+rewrite (Rmult_comm (Rabs x) (Rabs (x ^ n))).
+apply Rmult_le_compat_l.
+apply Rabs_pos.
+unfold Rgt in H.
+apply Rlt_le; assumption.
+Qed.
+
+Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n).
+Proof.
+intro; simple induction n; simpl in |- *.
+apply sym_eq; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1.
+intros; rewrite H; apply sym_eq; apply Rabs_mult.
+Qed.
+
+
+Lemma Pow_x_infinity :
+ forall x:R,
+   Rabs x > 1 ->
+   forall b:R,
+      exists N : nat | (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b).
+Proof.
+intros; elim (archimed (b * / (Rabs x - 1))); intros; clear H1;
+ cut ( exists N : nat | INR N >= b * / (Rabs x - 1)).
+intro; elim H1; clear H1; intros; exists x0; intros;
+ apply (Rge_trans (Rabs (x ^ n)) (Rabs (x ^ x0)) b).
+apply Rle_ge; apply Power_monotonic; assumption.
+rewrite <- RPow_abs; cut (Rabs x = 1 + (Rabs x - 1)).
+intro; rewrite H3;
+ apply (Rge_trans ((1 + (Rabs x - 1)) ^ x0) (1 + INR x0 * (Rabs x - 1)) b).
+apply Rle_ge; apply poly; fold (Rabs x - 1 > 0) in |- *; apply Rgt_minus;
+ assumption.
+apply (Rge_trans (1 + INR x0 * (Rabs x - 1)) (INR x0 * (Rabs x - 1)) b).
+apply Rle_ge; apply Rlt_le; rewrite (Rplus_comm 1 (INR x0 * (Rabs x - 1)));
+ pattern (INR x0 * (Rabs x - 1)) at 1 in |- *;
+ rewrite <- (let (H1, H2) := Rplus_ne (INR x0 * (Rabs x - 1)) in H1);
+ apply Rplus_lt_compat_l; apply Rlt_0_1.
+cut (b = b * / (Rabs x - 1) * (Rabs x - 1)).
+intros; rewrite H4; apply Rmult_ge_compat_r.
+apply Rge_minus; unfold Rge in |- *; left; assumption.
+assumption.
+rewrite Rmult_assoc; rewrite Rinv_l.
+ring.
+apply Rlt_dichotomy_converse; right; apply Rgt_minus; assumption.
+ring.
+cut ((0 <= up (b * / (Rabs x - 1)))%Z \/ (up (b * / (Rabs x - 1)) <= 0)%Z).
+intros; elim H1; intro.
+elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0;
+ apply
+  (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
+rewrite INR_IZR_INZ; apply IZR_ge; omega.
+unfold Rge in |- *; left; assumption.
+exists 0%nat;
+ apply
+  (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
+rewrite INR_IZR_INZ; apply IZR_ge; simpl in |- *; omega.
+unfold Rge in |- *; left; assumption.
+omega.
+Qed.
+
+Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.
+Proof.
+simple induction n.
+simpl in |- *; auto.
+intros; elim H; reflexivity.
+intros; simpl in |- *; apply Rmult_0_l.
+Qed.
+
+Lemma Rinv_pow : forall (x:R) (n:nat), x <> 0 -> / x ^ n = (/ x) ^ n.
+Proof.
+intros; elim n; simpl in |- *.
+apply Rinv_1.
+intro m; intro; rewrite Rinv_mult_distr.
+rewrite H0; reflexivity; assumption.
+assumption.
+apply pow_nonzero; assumption.
+Qed.
+
+Lemma pow_lt_1_zero :
+ forall x:R,
+   Rabs x < 1 ->
+   forall y:R,
+     0 < y ->
+      exists N : nat | (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y).
+Proof.
+intros; elim (Req_dec x 0); intro. 
+exists 1%nat; rewrite H1; intros n GE; rewrite pow_ne_zero.
+rewrite Rabs_R0; assumption.
+inversion GE; auto.
+cut (Rabs (/ x) > 1).
+intros; elim (Pow_x_infinity (/ x) H2 (/ y + 1)); intros N.
+exists N; intros; rewrite <- (Rinv_involutive y).
+rewrite <- (Rinv_involutive (Rabs (x ^ n))).
+apply Rinv_lt_contravar.
+apply Rmult_lt_0_compat.
+apply Rinv_0_lt_compat.
+assumption.
+apply Rinv_0_lt_compat.
+apply Rabs_pos_lt.
+apply pow_nonzero.
+assumption.
+rewrite <- Rabs_Rinv.
+rewrite Rinv_pow.
+apply (Rlt_le_trans (/ y) (/ y + 1) (Rabs ((/ x) ^ n))).
+pattern (/ y) at 1 in |- *.
+rewrite <- (let (H1, H2) := Rplus_ne (/ y) in H1).
+apply Rplus_lt_compat_l.
+apply Rlt_0_1.
+apply Rge_le.
+apply H3.
+assumption.
+assumption.
+apply pow_nonzero.
+assumption.
+apply Rabs_no_R0.
+apply pow_nonzero.
+assumption.
+apply Rlt_dichotomy_converse.
+right; unfold Rgt in |- *; assumption.
+rewrite <- (Rinv_involutive 1).
+rewrite Rabs_Rinv.
+unfold Rgt in |- *; apply Rinv_lt_contravar.
+apply Rmult_lt_0_compat.
+apply Rabs_pos_lt.
+assumption.
+rewrite Rinv_1; apply Rlt_0_1.
+rewrite Rinv_1; assumption.
+assumption.
+red in |- *; intro; apply R1_neq_R0; assumption.
+Qed.
+
+Lemma pow_R1 : forall (r:R) (n:nat), r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat.
+Proof.
+intros r n H'.
+case (Req_dec (Rabs r) 1); auto; intros H'1.
+case (Rdichotomy _ _ H'1); intros H'2.
+generalize H'; case n; auto.
+intros n0 H'0.
+cut (r <> 0); [ intros Eq1 | idtac ].
+cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
+absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0); auto.
+replace (Rabs (/ r) ^ S n0) with 1.
+simpl in |- *; apply Rlt_irrefl; auto.
+rewrite Rabs_Rinv; auto.
+rewrite <- Rinv_pow; auto.
+rewrite RPow_abs; auto.
+rewrite H'0; rewrite Rabs_right; auto with real.
+apply Rle_ge; auto with real.
+apply Rlt_pow; auto with arith.
+rewrite Rabs_Rinv; auto.
+apply Rmult_lt_reg_l with (r := Rabs r).
+case (Rabs_pos r); auto.
+intros H'3; case Eq2; auto.
+rewrite Rmult_1_r; rewrite Rinv_r; auto with real.
+red in |- *; intro; absurd (r ^ S n0 = 1); auto.
+simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real.
+generalize H'; case n; auto.
+intros n0 H'0.
+cut (r <> 0); [ intros Eq1 | auto with real ].
+cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
+absurd (Rabs r ^ 0 < Rabs r ^ S n0); auto with real arith.
+repeat rewrite RPow_abs; rewrite H'0; simpl in |- *; auto with real.
+red in |- *; intro; absurd (r ^ S n0 = 1); auto.
+simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real.
+Qed.
+
+Lemma pow_Rsqr : forall (x:R) (n:nat), x ^ (2 * n) = Rsqr x ^ n.
+Proof.
+intros; induction  n as [| n Hrecn].
+reflexivity.
+replace (2 * S n)%nat with (S (S (2 * n))).
+replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
+rewrite Hrecn; reflexivity.
+simpl in |- *; ring.
+apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
+ ring.
+Qed.
+
+Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
+Proof.
+intros; induction  n as [| n Hrecn].
+simpl in |- *; left; apply Rlt_0_1.
+simpl in |- *; apply Rmult_le_pos; assumption.
 Qed.
 
 (**********)
-Lemma pow_1_even : (n:nat) ``(pow (-1) (mult (S (S O)) n))==1``.
+Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.
 Proof.
-Intro; Induction n.
-Reflexivity.
-Replace (mult (2) (S n)) with (plus (2) (mult (2) n)).
-Rewrite pow_add; Rewrite Hrecn; Simpl; Ring.
-Replace (S n) with (plus n (1)); [Ring | Ring].
+intro; induction  n as [| n Hrecn].
+reflexivity.
+replace (2 * S n)%nat with (2 + 2 * n)%nat.
+rewrite pow_add; rewrite Hrecn; simpl in |- *; ring.
+replace (S n) with (n + 1)%nat; [ ring | ring ].
 Qed.
 
 (**********)
-Lemma pow_1_odd : (n:nat) ``(pow (-1) (S (mult (S (S O)) n)))==-1``.
+Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.
 Proof.
-Intro; Replace (S (mult (2) n)) with (plus (mult (2) n) (1)); [Idtac | Ring].
-Rewrite pow_add; Rewrite pow_1_even; Simpl; Ring.
+intro; replace (S (2 * n)) with (2 * n + 1)%nat; [ idtac | ring ].
+rewrite pow_add; rewrite pow_1_even; simpl in |- *; ring.
 Qed.
 
 (**********)
-Lemma pow_1_abs : (n:nat) ``(Rabsolu (pow (-1) n))==1``.
-Proof.
-Intro; Induction n.
-Simpl; Apply Rabsolu_R1.
-Replace (S n) with (plus n (1)); [Rewrite pow_add | Ring].
-Rewrite Rabsolu_mult.
-Rewrite Hrecn; Rewrite Rmult_1l; Simpl; Rewrite Rmult_1r; Rewrite Rabsolu_Ropp; Apply Rabsolu_R1.
-Qed.
-
-Lemma pow_mult : (x:R;n1,n2:nat) (pow x (mult n1 n2))==(pow (pow x n1) n2).
-Proof.
-Intros; Induction n2.
-Simpl; Replace (mult n1 O) with O; [Reflexivity | Ring].
-Replace (mult n1 (S n2)) with (plus (mult n1 n2) n1).
-Replace (S n2) with (plus n2 (1)); [Idtac | Ring].
-Do 2 Rewrite pow_add.
-Rewrite Hrecn2.
-Simpl.
-Ring.
-Apply INR_eq; Rewrite plus_INR; Do 2 Rewrite mult_INR; Rewrite S_INR; Ring.
-Qed.
-
-Lemma pow_incr : (x,y:R;n:nat) ``0<=x<=y`` -> ``(pow x n)<=(pow y n)``.
-Proof.
-Intros.
-Induction n.
-Right; Reflexivity.
-Simpl.
-Elim H; Intros.
-Apply Rle_trans with ``y*(pow x n)``.
-Do 2 Rewrite <- (Rmult_sym (pow x n)).
-Apply Rle_monotony.
-Apply pow_le; Assumption.
-Assumption.
-Apply Rle_monotony.
-Apply Rle_trans with x; Assumption.
-Apply Hrecn.
-Qed.
-
-Lemma pow_R1_Rle : (x:R;k:nat) ``1<=x`` -> ``1<=(pow x k)``.
-Proof.
-Intros.
-Induction k.
-Right; Reflexivity.
-Simpl.
-Apply Rle_trans with ``x*1``.
-Rewrite Rmult_1r; Assumption.
-Apply Rle_monotony.
-Left; Apply Rlt_le_trans with R1; [Apply Rlt_R0_R1 | Assumption].
-Exact Hreck.
-Qed.
-
-Lemma Rle_pow : (x:R;m,n:nat) ``1<=x`` -> (le m n) -> ``(pow x m)<=(pow x n)``.
-Proof.
-Intros.
-Replace n with (plus (minus n m) m).
-Rewrite pow_add.
-Rewrite Rmult_sym.
-Pattern 1 (pow x m); Rewrite <- Rmult_1r.
-Apply Rle_monotony.
-Apply pow_le; Left; Apply Rlt_le_trans with R1; [Apply Rlt_R0_R1 | Assumption].
-Apply pow_R1_Rle; Assumption.
-Rewrite plus_sym.
-Symmetry; Apply le_plus_minus; Assumption.
-Qed.
-
-Lemma pow1 : (n:nat) (pow R1 n)==R1.
-Proof.
-Intro; Induction n.
-Reflexivity.
-Simpl; Rewrite Hrecn; Rewrite Rmult_1r; Reflexivity.
-Qed.
-
-Lemma pow_Rabs : (x:R;n:nat) ``(pow x n)<=(pow (Rabsolu x) n)``.
-Proof.
-Intros; Induction n.
-Right; Reflexivity.
-Simpl; Case (case_Rabsolu x); Intro.
-Apply Rle_trans with (Rabsolu ``x*(pow x n)``).
-Apply Rle_Rabsolu.
-Rewrite Rabsolu_mult.
-Apply Rle_monotony.
-Apply Rabsolu_pos.
-Right; Symmetry; Apply Pow_Rabsolu.
-Pattern 1 (Rabsolu x); Rewrite (Rabsolu_right x r); Apply Rle_monotony.
-Apply Rle_sym2; Exact r.
-Apply Hrecn.
-Qed.
-
-Lemma pow_maj_Rabs : (x,y:R;n:nat) ``(Rabsolu y)<=x`` -> ``(pow y n)<=(pow x n)``.
-Proof.
-Intros; Cut ``0<=x``.
-Intro; Apply Rle_trans with (pow (Rabsolu y) n).
-Apply pow_Rabs.
-Induction n.
-Right; Reflexivity.
-Simpl; Apply Rle_trans with ``x*(pow (Rabsolu y) n)``.
-Do 2 Rewrite <- (Rmult_sym (pow (Rabsolu y) n)).
-Apply Rle_monotony.
-Apply pow_le; Apply Rabsolu_pos.
-Assumption.
-Apply Rle_monotony.
-Apply H0.
-Apply Hrecn.
-Apply Rle_trans with (Rabsolu y); [Apply Rabsolu_pos | Exact H].
+Lemma pow_1_abs : forall n:nat, Rabs ((-1) ^ n) = 1.
+Proof.
+intro; induction  n as [| n Hrecn].
+simpl in |- *; apply Rabs_R1.
+replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ].
+rewrite Rabs_mult.
+rewrite Hrecn; rewrite Rmult_1_l; simpl in |- *; rewrite Rmult_1_r;
+ rewrite Rabs_Ropp; apply Rabs_R1.
+Qed.
+
+Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = x ^ n1 ^ n2.
+Proof.
+intros; induction  n2 as [| n2 Hrecn2].
+simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
+replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat.
+replace (S n2) with (n2 + 1)%nat; [ idtac | ring ].
+do 2 rewrite pow_add.
+rewrite Hrecn2.
+simpl in |- *.
+ring.
+apply INR_eq; rewrite plus_INR; do 2 rewrite mult_INR; rewrite S_INR; ring.
+Qed.
+
+Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
+Proof.
+intros.
+induction  n as [| n Hrecn].
+right; reflexivity.
+simpl in |- *.
+elim H; intros.
+apply Rle_trans with (y * x ^ n).
+do 2 rewrite <- (Rmult_comm (x ^ n)).
+apply Rmult_le_compat_l.
+apply pow_le; assumption.
+assumption.
+apply Rmult_le_compat_l.
+apply Rle_trans with x; assumption.
+apply Hrecn.
+Qed.
+
+Lemma pow_R1_Rle : forall (x:R) (k:nat), 1 <= x -> 1 <= x ^ k.
+Proof.
+intros.
+induction  k as [| k Hreck].
+right; reflexivity.
+simpl in |- *.
+apply Rle_trans with (x * 1).
+rewrite Rmult_1_r; assumption.
+apply Rmult_le_compat_l.
+left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ].
+exact Hreck.
+Qed.
+
+Lemma Rle_pow :
+ forall (x:R) (m n:nat), 1 <= x -> (m <= n)%nat -> x ^ m <= x ^ n.
+Proof.
+intros.
+replace n with (n - m + m)%nat.
+rewrite pow_add.
+rewrite Rmult_comm.
+pattern (x ^ m) at 1 in |- *; rewrite <- Rmult_1_r.
+apply Rmult_le_compat_l.
+apply pow_le; left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ].
+apply pow_R1_Rle; assumption.
+rewrite plus_comm.
+symmetry  in |- *; apply le_plus_minus; assumption.
+Qed.
+
+Lemma pow1 : forall n:nat, 1 ^ n = 1.
+Proof.
+intro; induction  n as [| n Hrecn].
+reflexivity.
+simpl in |- *; rewrite Hrecn; rewrite Rmult_1_r; reflexivity.
+Qed.
+
+Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n.
+Proof.
+intros; induction  n as [| n Hrecn].
+right; reflexivity.
+simpl in |- *; case (Rcase_abs x); intro.
+apply Rle_trans with (Rabs (x * x ^ n)).
+apply RRle_abs.
+rewrite Rabs_mult.
+apply Rmult_le_compat_l.
+apply Rabs_pos.
+right; symmetry  in |- *; apply RPow_abs.
+pattern (Rabs x) at 1 in |- *; rewrite (Rabs_right x r);
+ apply Rmult_le_compat_l.
+apply Rge_le; exact r.
+apply Hrecn.
+Qed.
+
+Lemma pow_maj_Rabs : forall (x y:R) (n:nat), Rabs y <= x -> y ^ n <= x ^ n.
+Proof.
+intros; cut (0 <= x).
+intro; apply Rle_trans with (Rabs y ^ n).
+apply pow_Rabs.
+induction  n as [| n Hrecn].
+right; reflexivity.
+simpl in |- *; apply Rle_trans with (x * Rabs y ^ n).
+do 2 rewrite <- (Rmult_comm (Rabs y ^ n)).
+apply Rmult_le_compat_l.
+apply pow_le; apply Rabs_pos.
+assumption.
+apply Rmult_le_compat_l.
+apply H0.
+apply Hrecn.
+apply Rle_trans with (Rabs y); [ apply Rabs_pos | exact H ].
 Qed.
 
 (*******************************)
@@ -556,207 +524,200 @@ Qed.
 (*******************************)
 (*i Due to L.Thery i*)
 
-Tactic Definition CaseEqk name :=
-Generalize (refl_equal ? name); Pattern -1 name; Case name.
+Ltac case_eq name :=
+  generalize (refl_equal name); pattern name at -1 in |- *; case name.
 
-Definition powerRZ :=
-   [x : R] [n : Z]  Cases n of
-                      ZERO => R1
-                     | (POS p) => (pow x (convert p))
-                     | (NEG p) => (Rinv (pow x (convert p)))
-                    end.
+Definition powerRZ (x:R) (n:Z) :=
+  match n with
+  | Z0 => 1
+  | Zpos p => x ^ nat_of_P p
+  | Zneg p => / x ^ nat_of_P p
+  end.
 
-Infix Local "^Z" powerRZ (at level 2, left associativity) : R_scope.
+Infix Local "^Z" := powerRZ (at level 30, left associativity) : R_scope.
 
-Lemma Zpower_NR0:
- (x : Z) (n : nat) (Zle ZERO x) ->  (Zle ZERO (Zpower_nat x n)).
+Lemma Zpower_NR0 :
+ forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z.
 Proof.
-NewInduction n; Unfold Zpower_nat; Simpl; Auto with zarith.
+induction n; unfold Zpower_nat in |- *; simpl in |- *; auto with zarith.
 Qed.
 
-Lemma powerRZ_O: (x : R)  (powerRZ x ZERO) == R1.
+Lemma powerRZ_O : forall x:R, x ^Z 0 = 1.
 Proof.
-Reflexivity.
+reflexivity.
 Qed.
  
-Lemma powerRZ_1: (x : R)  (powerRZ x (Zs ZERO)) == x.
+Lemma powerRZ_1 : forall x:R, x ^Z Zsucc 0 = x.
 Proof.
-Simpl; Auto with real.
+simpl in |- *; auto with real.
 Qed.
  
-Lemma powerRZ_NOR: (x : R) (z : Z) ~ x == R0 ->  ~ (powerRZ x z) == R0.
+Lemma powerRZ_NOR : forall (x:R) (z:Z), x <> 0 -> x ^Z z <> 0.
 Proof.
-NewDestruct z; Simpl; Auto with real.
+destruct z; simpl in |- *; auto with real.
 Qed.
  
-Lemma powerRZ_add:
- (x : R)
- (n, m : Z)
- ~ x == R0 ->  (powerRZ x (Zplus n m)) == (Rmult (powerRZ x n) (powerRZ x m)).
+Lemma powerRZ_add :
+ forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m.
 Proof.
-Intro x; NewDestruct n as [|n1|n1]; NewDestruct m as [|m1|m1]; Simpl;
-  Auto with real.
+intro x; destruct n as [| n1| n1]; destruct m as [| m1| m1]; simpl in |- *;
+ auto with real.
 (* POS/POS *)
-Rewrite convert_add; Auto with real.
+rewrite nat_of_P_plus_morphism; auto with real.
 (* POS/NEG *)
-(CaseEqk '(compare n1 m1 EGAL)); Simpl; Auto with real.
-Intros H' H'0; Rewrite compare_convert_EGAL with 1 := H'; Auto with real.
-Intros H' H'0; Rewrite (true_sub_convert m1 n1); Auto with real.
-Rewrite (pow_RN_plus x (minus (convert m1) (convert n1)) (convert n1));
- Auto with real.
-Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
-Rewrite Rinv_Rmult; Auto with real.
-Rewrite Rinv_Rinv; Auto with real.
-Apply lt_le_weak.
-Apply compare_convert_INFERIEUR; Auto.
-Apply ZC2; Auto.
-Intros H' H'0; Rewrite (true_sub_convert n1 m1); Auto with real.
-Rewrite (pow_RN_plus x (minus (convert n1) (convert m1)) (convert m1));
- Auto with real.
-Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
-Apply lt_le_weak.
-Change (gt (convert n1) (convert m1)).
-Apply compare_convert_SUPERIEUR; Auto.
+case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real.
+intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
+intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
+rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
+ auto with real.
+rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
+rewrite Rinv_mult_distr; auto with real.
+rewrite Rinv_involutive; auto with real.
+apply lt_le_weak.
+apply nat_of_P_lt_Lt_compare_morphism; auto.
+apply ZC2; auto.
+intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
+rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
+ auto with real.
+rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
+apply lt_le_weak.
+change (nat_of_P n1 > nat_of_P m1)%nat in |- *.
+apply nat_of_P_gt_Gt_compare_morphism; auto.
 (* NEG/POS *)
-(CaseEqk '(compare n1 m1 EGAL)); Simpl; Auto with real.
-Intros H' H'0; Rewrite compare_convert_EGAL with 1 := H'; Auto with real.
-Intros H' H'0; Rewrite (true_sub_convert m1 n1); Auto with real.
-Rewrite (pow_RN_plus x (minus (convert m1) (convert n1)) (convert n1));
- Auto with real.
-Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
-Apply lt_le_weak.
-Apply compare_convert_INFERIEUR; Auto.
-Apply ZC2; Auto.
-Intros H' H'0; Rewrite (true_sub_convert n1 m1); Auto with real.
-Rewrite (pow_RN_plus x (minus (convert n1) (convert m1)) (convert m1));
- Auto with real.
-Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
-Rewrite Rinv_Rmult; Auto with real.
-Apply lt_le_weak.
-Change (gt (convert n1) (convert m1)).
-Apply compare_convert_SUPERIEUR; Auto.
+case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real.
+intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
+intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
+rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
+ auto with real.
+rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
+apply lt_le_weak.
+apply nat_of_P_lt_Lt_compare_morphism; auto.
+apply ZC2; auto.
+intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
+rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
+ auto with real.
+rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
+rewrite Rinv_mult_distr; auto with real.
+apply lt_le_weak.
+change (nat_of_P n1 > nat_of_P m1)%nat in |- *.
+apply nat_of_P_gt_Gt_compare_morphism; auto.
 (* NEG/NEG *)
-Rewrite convert_add; Auto with real.
-Intros H'; Rewrite pow_add; Auto with real.
-Apply Rinv_Rmult; Auto.
-Apply pow_nonzero; Auto.
-Apply pow_nonzero; Auto.
+rewrite nat_of_P_plus_morphism; auto with real.
+intros H'; rewrite pow_add; auto with real.
+apply Rinv_mult_distr; auto.
+apply pow_nonzero; auto.
+apply pow_nonzero; auto.
 Qed.
-Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add :real.
+Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.
  
-Lemma Zpower_nat_powerRZ:
- (n, m : nat)
-  (IZR (Zpower_nat (inject_nat n) m)) == (powerRZ (INR n) (inject_nat m)).
-Proof.
-Intros n m; Elim m; Simpl; Auto with real.
-Intros m1 H'; Rewrite bij1; Simpl.
-Replace (Zpower_nat (inject_nat n) (S m1))
-     with (Zmult (inject_nat n) (Zpower_nat (inject_nat n) m1)).
-Rewrite mult_IZR; Auto with real.
-Repeat Rewrite <- INR_IZR_INZ; Simpl.
-Rewrite H'; Simpl.
-Case m1; Simpl; Auto with real.
-Intros m2; Rewrite bij1; Auto.
-Unfold Zpower_nat; Auto.
+Lemma Zpower_nat_powerRZ :
+ forall n m:nat, IZR (Zpower_nat (Z_of_nat n) m) = INR n ^Z Z_of_nat m.
+Proof.
+intros n m; elim m; simpl in |- *; auto with real.
+intros m1 H'; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; simpl in |- *.
+replace (Zpower_nat (Z_of_nat n) (S m1)) with
+ (Z_of_nat n * Zpower_nat (Z_of_nat n) m1)%Z.
+rewrite mult_IZR; auto with real.
+repeat rewrite <- INR_IZR_INZ; simpl in |- *.
+rewrite H'; simpl in |- *.
+case m1; simpl in |- *; auto with real.
+intros m2; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto.
+unfold Zpower_nat in |- *; auto.
 Qed.
  
-Lemma powerRZ_lt: (x : R) (z : Z) (Rlt R0 x) ->  (Rlt R0 (powerRZ x z)).
+Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z.
 Proof.
-Intros x z; Case z; Simpl; Auto with real.
+intros x z; case z; simpl in |- *; auto with real.
 Qed.
-Hints Resolve powerRZ_lt :real.
+Hint Resolve powerRZ_lt: real.
  
-Lemma powerRZ_le: (x : R) (z : Z) (Rlt R0 x) ->  (Rle R0 (powerRZ x z)).
+Lemma powerRZ_le : forall (x:R) (z:Z), 0 < x -> 0 <= x ^Z z.
 Proof.
-Intros x z H'; Apply Rlt_le; Auto with real.
+intros x z H'; apply Rlt_le; auto with real.
 Qed.
-Hints Resolve powerRZ_le :real.
+Hint Resolve powerRZ_le: real.
  
-Lemma Zpower_nat_powerRZ_absolu:
- (n, m : Z)
- (Zle ZERO m) ->  (IZR (Zpower_nat n (absolu m))) == (powerRZ (IZR n) m).
+Lemma Zpower_nat_powerRZ_absolu :
+ forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Zabs_nat m)) = IZR n ^Z m.
 Proof.
-Intros n m; Case m; Simpl; Auto with zarith.
-Intros p H'; Elim (convert p); Simpl; Auto with zarith.
-Intros n0 H'0; Rewrite <- H'0; Simpl; Auto with zarith.
-Rewrite <- mult_IZR; Auto.
-Intros p H'; Absurd `0 <= (NEG p)`;Auto with zarith.
+intros n m; case m; simpl in |- *; auto with zarith.
+intros p H'; elim (nat_of_P p); simpl in |- *; auto with zarith.
+intros n0 H'0; rewrite <- H'0; simpl in |- *; auto with zarith.
+rewrite <- mult_IZR; auto.
+intros p H'; absurd (0 <= Zneg p)%Z; auto with zarith.
 Qed.
 
-Lemma powerRZ_R1: (n : Z)  (powerRZ R1 n) == R1.
+Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1.
 Proof.
-Intros n; Case n; Simpl; Auto.
-Intros p; Elim (convert p); Simpl; Auto; Intros n0 H'; Rewrite H'; Ring.
-Intros p; Elim (convert p); Simpl.
-Exact Rinv_R1.
-Intros n1 H'; Rewrite Rinv_Rmult; Try Rewrite Rinv_R1; Try Rewrite H';
- Auto with real.
+intros n; case n; simpl in |- *; auto.
+intros p; elim (nat_of_P p); simpl in |- *; auto; intros n0 H'; rewrite H';
+ ring.
+intros p; elim (nat_of_P p); simpl in |- *.
+exact Rinv_1.
+intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H';
+ auto with real.
 Qed.
 
 (*******************************)
 (** Sum of n first naturals    *)
 (*******************************)
 (*********)
-Fixpoint sum_nat_f_O [f:nat->nat;n:nat]:nat:=       
-  Cases n of                            
-    O => (f O)                               
-   |(S n') => (plus (sum_nat_f_O f n') (f (S n'))) 
+Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat :=
+  match n with
+  | O => f 0%nat
+  | S n' => (sum_nat_f_O f n' + f (S n'))%nat
   end.
 
 (*********)
-Definition sum_nat_f [s,n:nat;f:nat->nat]:nat:=      
-  (sum_nat_f_O [x:nat](f (plus x s)) (minus n s)).
+Definition sum_nat_f (s n:nat) (f:nat -> nat) : nat :=
+  sum_nat_f_O (fun x:nat => f (x + s)%nat) (n - s).
 
 (*********)
-Definition sum_nat_O [n:nat]:nat:=
-  (sum_nat_f_O [x:nat]x n).
+Definition sum_nat_O (n:nat) : nat := sum_nat_f_O (fun x:nat => x) n.
 
 (*********)
-Definition sum_nat [s,n:nat]:nat:=
-  (sum_nat_f s n [x:nat]x).
+Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x).
 
 (*******************************)
 (**            Sum             *)
 (*******************************)
 (*********)
-Fixpoint sum_f_R0 [f:nat->R;N:nat]:R:=
-  Cases N of
-     O     => (f O)
-    |(S i) => (Rplus (sum_f_R0 f i) (f (S i)))
+Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R :=
+  match N with
+  | O => f 0%nat
+  | S i => sum_f_R0 f i + f (S i)
   end.
 
 (*********)
-Definition sum_f [s,n:nat;f:nat->R]:R:=      
-  (sum_f_R0 [x:nat](f (plus x s)) (minus n s)).
-
-Lemma GP_finite:
-  (x:R) (n:nat) (Rmult (sum_f_R0 [n:nat] (pow x n) n)
-                       (Rminus x R1)) ==
-                (Rminus (pow x (plus n (1))) R1).
-Proof.
-Intros; Induction n; Simpl.
-Ring.
-Rewrite Rmult_Rplus_distrl;Rewrite Hrecn;Cut (plus n (1))=(S n).
-Intro H;Rewrite H;Simpl;Ring.
-Omega.
-Qed.
-
-Lemma sum_f_R0_triangle:
-  (x:nat->R)(n:nat) (Rle (Rabsolu (sum_f_R0 x n))
-                         (sum_f_R0 [i:nat] (Rabsolu (x i)) n)).
-Proof.
-Intro; Induction n; Simpl.
-Unfold Rle; Right; Reflexivity.
-Intro m; Intro;Apply (Rle_trans
-          (Rabsolu (Rplus (sum_f_R0 x m) (x (S m))))
-          (Rplus (Rabsolu (sum_f_R0 x m))
-                 (Rabsolu (x (S m))))
-          (Rplus (sum_f_R0 [i:nat](Rabsolu (x i)) m) 
-                 (Rabsolu (x (S m))))).
-Apply Rabsolu_triang.
-Rewrite Rplus_sym;Rewrite (Rplus_sym 
-  (sum_f_R0 [i:nat](Rabsolu (x i)) m) (Rabsolu (x (S m))));
-  Apply Rle_compatibility;Assumption.
+Definition sum_f (s n:nat) (f:nat -> R) : R :=
+  sum_f_R0 (fun x:nat => f (x + s)%nat) (n - s).
+
+Lemma GP_finite :
+ forall (x:R) (n:nat),
+   sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1.
+Proof.
+intros; induction  n as [| n Hrecn]; simpl in |- *.
+ring.
+rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n).
+intro H; rewrite H; simpl in |- *; ring.
+omega.
+Qed.
+
+Lemma sum_f_R0_triangle :
+ forall (x:nat -> R) (n:nat),
+   Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n.
+Proof.
+intro; simple induction n; simpl in |- *.
+unfold Rle in |- *; right; reflexivity.
+intro m; intro;
+ apply
+  (Rle_trans (Rabs (sum_f_R0 x m + x (S m)))
+     (Rabs (sum_f_R0 x m) + Rabs (x (S m)))
+     (sum_f_R0 (fun i:nat => Rabs (x i)) m + Rabs (x (S m)))).
+apply Rabs_triang.
+rewrite Rplus_comm;
+ rewrite (Rplus_comm (sum_f_R0 (fun i:nat => Rabs (x i)) m) (Rabs (x (S m))));
+ apply Rplus_le_compat_l; assumption.
 Qed.
 
 (*******************************)
@@ -764,69 +725,69 @@ Qed.
 (*******************************)
 
 (*********)
-Definition R_dist:R->R->R:=[x,y:R](Rabsolu (Rminus x y)).
+Definition R_dist (x y:R) : R := Rabs (x - y).
 
 (*********)
-Lemma R_dist_pos:(x,y:R)(Rge (R_dist x y) R0).
+Lemma R_dist_pos : forall x y:R, R_dist x y >= 0.
 Proof.
-Intros;Unfold R_dist;Unfold Rabsolu;Case (case_Rabsolu (Rminus x y));Intro l.
-Unfold Rge;Left;Apply (Rlt_RoppO (Rminus x y) l).
-Trivial.
+intros; unfold R_dist in |- *; unfold Rabs in |- *; case (Rcase_abs (x - y));
+ intro l.
+unfold Rge in |- *; left; apply (Ropp_gt_lt_0_contravar (x - y) l).
+trivial.
 Qed.
 
 (*********)
-Lemma R_dist_sym:(x,y:R)(R_dist x y)==(R_dist y x).
+Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x.
 Proof.
-Unfold R_dist;Intros;SplitAbsolu;Ring.
-Generalize (Rlt_RoppO (Rminus y x) r); Intro;
- Rewrite (Ropp_distr2 y x) in H;
- Generalize (Rlt_antisym (Rminus x y) R0 r0); Intro;Unfold Rgt in H;
- ElimType False; Auto.
-Generalize (minus_Rge y x r); Intro;
- Generalize (minus_Rge x y r0); Intro;
- Generalize (Rge_ge_eq x y H0 H); Intro;Rewrite H1;Ring.
+unfold R_dist in |- *; intros; split_Rabs; ring.
+generalize (Ropp_gt_lt_0_contravar (y - x) r); intro;
+ rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0);
+ intro; unfold Rgt in H; elimtype False; auto.
+generalize (minus_Rge y x r); intro; generalize (minus_Rge x y r0); intro;
+ generalize (Rge_antisym x y H0 H); intro; rewrite H1; 
+ ring.
 Qed.
 
 (*********)
-Lemma R_dist_refl:(x,y:R)((R_dist x y)==R0<->x==y).
+Lemma R_dist_refl : forall x y:R, R_dist x y = 0 <-> x = y.
 Proof.
-Unfold R_dist;Intros;SplitAbsolu;Split;Intros.
-Rewrite (Ropp_distr2 x y) in H;Apply sym_eqT;
- Apply (Rminus_eq y x H).
-Rewrite (Ropp_distr2 x y);Generalize (sym_eqT R x y H);Intro;
- Apply (eq_Rminus y x H0).
-Apply (Rminus_eq x y H).
-Apply (eq_Rminus x y H). 
+unfold R_dist in |- *; intros; split_Rabs; split; intros.
+rewrite (Ropp_minus_distr x y) in H; apply sym_eq;
+ apply (Rminus_diag_uniq y x H).
+rewrite (Ropp_minus_distr x y); generalize (sym_eq H); intro;
+ apply (Rminus_diag_eq y x H0).
+apply (Rminus_diag_uniq x y H).
+apply (Rminus_diag_eq x y H). 
 Qed.
 
-Lemma R_dist_eq:(x:R)(R_dist x x)==R0.
+Lemma R_dist_eq : forall x:R, R_dist x x = 0.
 Proof.
-Unfold R_dist;Intros;SplitAbsolu;Intros;Ring.
+unfold R_dist in |- *; intros; split_Rabs; intros; ring.
 Qed.
 
 (***********)
-Lemma R_dist_tri:(x,y,z:R)(Rle (R_dist x y) 
-                   (Rplus (R_dist x z) (R_dist z y))).
+Lemma R_dist_tri : forall x y z:R, R_dist x y <= R_dist x z + R_dist z y.
 Proof.
-Intros;Unfold R_dist; Replace ``x-y`` with ``(x-z)+(z-y)``;
-  [Apply (Rabsolu_triang ``x-z`` ``z-y``)|Ring].
+intros; unfold R_dist in |- *; replace (x - y) with (x - z + (z - y));
+ [ apply (Rabs_triang (x - z) (z - y)) | ring ].
 Qed.
 
 (*********)
-Lemma R_dist_plus: (a,b,c,d:R)(Rle (R_dist (Rplus a c) (Rplus b d))
-                   (Rplus (R_dist a b) (R_dist c d))).
+Lemma R_dist_plus :
+ forall a b c d:R, R_dist (a + c) (b + d) <= R_dist a b + R_dist c d.
 Proof.
-Intros;Unfold R_dist;
- Replace (Rminus (Rplus a c) (Rplus b d))
-  with (Rplus (Rminus a b) (Rminus c d)).
-Exact (Rabsolu_triang (Rminus a b) (Rminus c d)).
-Ring.
+intros; unfold R_dist in |- *;
+ replace (a + c - (b + d)) with (a - b + (c - d)).
+exact (Rabs_triang (a - b) (c - d)).
+ring.
 Qed.
 
 (*******************************)
 (**       Infinit Sum          *)
 (*******************************)
 (*********)
-Definition infinit_sum:(nat->R)->R->Prop:=[s:nat->R;l:R]
-  (eps:R)(Rgt eps R0)->
-  (Ex[N:nat](n:nat)(ge n N)->(Rlt (R_dist (sum_f_R0 s n) l) eps)).
+Definition infinit_sum (s:nat -> R) (l:R) : Prop :=
+  forall eps:R,
+    eps > 0 ->
+     exists N : nat
+    | (forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps).
\ No newline at end of file