Notations pour l'exponentiation

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

1 files changed, 135 insertions, 77 deletions

diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index e9316e1ad..af5fda9d3 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -34,11 +34,13 @@ Open Local Scope R_scope.
 (*******************************)
 (*********)
 Lemma INR_fact_neq_0:(n:nat)~(INR (fact n))==R0.
+Proof.
 Intro;Red;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)).
+Proof.
 Intro; Reflexivity.
 Qed. 
 
@@ -46,6 +48,7 @@ Qed.
 Lemma simpl_fact:(n:nat)(Rmult (Rinv (INR (fact (S n)))) 
          (Rinv (Rinv (INR (fact n)))))==
          (Rinv (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));
@@ -67,24 +70,28 @@ Fixpoint pow [r:R;n:nat]:R:=
     |(S n) => (Rmult r (pow r n))
   end.
 
-Infix "^" pow (at level 2, left associativity) : R_scope.
+Infix "^" pow (at level 2, left associativity) : R_scope V8only.
 
-Lemma pow_O: (e : R)  (pow e O) == R1.
-Simpl; Auto with real.
+Lemma pow_O: (x : R)  (pow x O) == R1.
+Proof.
+Reflexivity.
 Qed.
  
-Lemma pow_1: (e : R)  (pow e (1)) == e.
+Lemma pow_1: (x : R)  (pow x (1)) == x.
+Proof.
 Simpl; Auto with real.
 Qed.
  
 Lemma pow_add:
- (e : R) (n, m : nat)  (pow e (plus n m)) == (Rmult (pow e n) (pow e m)).
-Intros e n; Elim n; Simpl; Auto with real.
+ (x : R) (n, m : nat)  (pow x (plus n m)) == (Rmult (pow x n) (pow x m)).
+Proof.
+Intros x n; Elim n; Simpl; 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).
+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).
@@ -95,29 +102,32 @@ Qed.
 Hints Resolve pow_O pow_1 pow_add pow_nonzero:real.
  
 Lemma pow_RN_plus:
- (e : R)
+ (x : R)
  (n, m : nat)
- ~ e == R0 ->  (pow e n) == (Rmult (pow e (plus n m)) (Rinv (pow e m))).
-Intros e n; Elim n; Simpl; Auto with real.
+ ~ 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: (e : R) (n : nat) (Rlt R0 e) ->  (Rlt R0 (pow e n)).
-Intros e n; Elim n; Simpl; Auto with real.
-Intros n0 H' H'0; Replace R0 with (Rmult e R0); Auto with real.
+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:
- (e : R) (n : nat) (Rlt R1 e) -> (lt O n) ->  (Rlt R1 (pow e n)).
-Intros e n; Elim n; Simpl; Auto with real.
+ (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 e 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.
@@ -125,14 +135,15 @@ Qed.
 Hints Resolve Rlt_pow_R1 :real.
 
 Lemma Rlt_pow:
- (e : R) (n, m : nat) (Rlt R1 e) -> (lt n m) ->  (Rlt (pow e n) (pow e m)).
-Intros e n m H' H'0; Replace m with (plus (minus m n) n).
+ (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 e n); Replace (pow e n) with (Rmult R1 (pow e n)); 
+Pattern 1 (pow x n); Replace (pow x n) with (Rmult R1 (pow x n)); 
  Auto with real.
 Apply Rminus_lt.
-Repeat Rewrite [x : R]  (Rmult_sym x (pow e n)); Rewrite <- Rminus_distr.
-Replace R0 with (Rmult (pow e n) R0); Auto with real.
+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.
@@ -146,6 +157,7 @@ Hints Resolve Rlt_pow :real.
 
 (*********)
 Lemma tech_pow_Rmult:(x:R)(n:nat)(Rmult x (pow x n))==(pow x (S n)).
+Proof.
 Induction n; Simpl; Trivial.
 Qed.
 
@@ -153,6 +165,7 @@ 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));
@@ -161,34 +174,35 @@ Intros; Pattern 1 (pow x a);
  Apply Rmult_sym.
 Qed.
 
-Lemma poly: (n:nat)(e:R)(Rlt R0 e)->
- (Rle (Rplus R1 (Rmult (INR n) e)) (pow  (Rplus R1 e) n)).
+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 e))==R1.
+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)) e))
-    (Rmult (Rplus R1 e) (Rplus R1 (Rmult (INR n0) e))) 
-    (Rmult (Rplus R1 e) (pow (Rplus R1 e) n0))).
-Cut (Rmult (Rplus R1 e) (Rplus R1 (Rmult (INR n0) e)))== 
-  (Rplus (Rplus R1 (Rmult (INR (S n0)) e)) 
-         (Rmult (INR n0) (Rmult e e))).
-Intro;Rewrite H1;Pattern 1 (Rplus R1 (Rmult (INR (S n0)) e));
+ 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)) e))) in H1);
+   (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 e);Apply (H3 (INR (S n1)) (Rsqr e) 
-        (lt_INR_0 (S n1) (lt_O_Sn n1)));Fold (Rgt e R0) in H;
- Apply (pos_Rsqr1 e (imp_not_Req e R0 
-  (or_intror (Rlt e R0) (Rgt e R0) H))).
+ 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 e (Rlt_le R0 e H)).
+ Apply (Rlt_r_plus_R1 x (Rlt_le R0 x H)).
 Assumption.
 Rewrite H1;Unfold Rle;Right;Trivial.
 Qed.
@@ -197,6 +211,7 @@ 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.
@@ -216,6 +231,7 @@ 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.
@@ -226,6 +242,7 @@ 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))))).
@@ -281,6 +298,7 @@ Qed.
 
 Lemma pow_ne_zero:
   (n:nat) ~(n=(0))-> (pow R0 n) == R0.
+Proof.
 Induction n.
 Simpl;Auto.
 Intros;Elim H;Reflexivity.
@@ -289,6 +307,7 @@ 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.
@@ -299,16 +318,17 @@ Qed.
 
 Lemma pow_lt_1_zero:
   (x:R) (Rlt (Rabsolu x) R1)
-        -> (e:R) (Rlt R0 e) 
+        -> (y:R) (Rlt R0 y) 
                  -> (Ex[N:nat] (n:nat) (ge n N)
-                         -> (Rlt (Rabsolu (pow x n)) e)).
+                         -> (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 e) R1));Intros N.
-Exists N;Intros;Rewrite <- (Rinv_Rinv e).
+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.
@@ -320,12 +340,12 @@ Apply pow_nonzero.
 Assumption.
 Rewrite <- Rabsolu_Rinv.
 Rewrite Rinv_pow.
-Apply (Rlt_le_trans (Rinv e)
-                    (Rplus (Rinv e) R1)
+Apply (Rlt_le_trans (Rinv y)
+                    (Rplus (Rinv y) R1)
                     (Rabsolu (pow (Rinv x) n))).
-Pattern 1 (Rinv e).
+Pattern 1 (Rinv y).
 Rewrite <- (let (H1,H2) = 
-                (Rplus_ne (Rinv e)) in H1).
+                (Rplus_ne (Rinv y)) in H1).
 Apply Rlt_compatibility.
 Apply Rlt_R0_R1.
 Apply Rle_sym2.
@@ -353,6 +373,7 @@ 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.
@@ -387,6 +408,7 @@ 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))).
@@ -397,6 +419,7 @@ Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; R
 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.
@@ -404,6 +427,7 @@ Qed.
 
 (**********)
 Lemma pow_1_even : (n:nat) ``(pow (-1) (mult (S (S O)) n))==1``.
+Proof.
 Intro; Induction n.
 Reflexivity.
 Replace (mult (2) (S n)) with (plus (2) (mult (2) n)).
@@ -413,12 +437,14 @@ Qed.
 
 (**********)
 Lemma pow_1_odd : (n:nat) ``(pow (-1) (S (mult (S (S O)) 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.
 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].
@@ -427,6 +453,7 @@ Rewrite Hrecn; Rewrite Rmult_1l; Simpl; Rewrite Rmult_1r; Rewrite Rabsolu_Ropp;
 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).
@@ -439,6 +466,7 @@ 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.
@@ -455,6 +483,7 @@ Apply Hrecn.
 Qed.
 
 Lemma pow_R1_Rle : (x:R;k:nat) ``1<=x`` -> ``1<=(pow x k)``.
+Proof.
 Intros.
 Induction k.
 Right; Reflexivity.
@@ -467,6 +496,7 @@ 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.
@@ -480,12 +510,14 @@ 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.
@@ -501,6 +533,7 @@ 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.
@@ -526,39 +559,49 @@ Tactic Definition CaseEqk name :=
 Generalize (refl_equal ? name); Pattern -1 name; Case name.
 
 Definition powerRZ :=
-   [e : R] [n : Z]  Cases n of
+   [x : R] [n : Z]  Cases n of
                       ZERO => R1
-                     | (POS p) => (pow e (convert p))
-                     | (NEG p) => (Rinv (pow e (convert p)))
+                     | (POS p) => (pow x (convert p))
+                     | (NEG p) => (Rinv (pow x (convert p)))
                     end.
 
+Infix Local "^Z" powerRZ (at level 2, left associativity) : R_scope.
+
 Lemma Zpower_NR0:
- (e : Z) (n : nat) (Zle ZERO e) ->  (Zle ZERO (Zpower_nat e n)).
-Intros e n; Elim n; Unfold Zpower_nat; Simpl; Auto with zarith.
+ (x : Z) (n : nat) (Zle ZERO x) ->  (Zle ZERO (Zpower_nat x n)).
+Proof.
+NewInduction n; Unfold Zpower_nat; Simpl; Auto with zarith.
 Qed.
 
-Lemma powerRZ_O: (e : R)  (powerRZ e ZERO) == R1.
-Simpl; Auto.
+Lemma powerRZ_O: (x : R)  (powerRZ x ZERO) == R1.
+Proof.
+Reflexivity.
 Qed.
  
-Lemma powerRZ_1: (e : R)  (powerRZ e (Zs ZERO)) == e.
+Lemma powerRZ_1: (x : R)  (powerRZ x (Zs ZERO)) == x.
+Proof.
 Simpl; Auto with real.
 Qed.
  
-Lemma powerRZ_NOR: (e : R) (z : Z) ~ e == R0 ->  ~ (powerRZ e z) == R0.
-Intros e z; Case z; Simpl; Auto with real.
+Lemma powerRZ_NOR: (x : R) (z : Z) ~ x == R0 ->  ~ (powerRZ x z) == R0.
+Proof.
+NewDestruct z; Simpl; Auto with real.
 Qed.
  
 Lemma powerRZ_add:
- (e : R)
+ (x : R)
  (n, m : Z)
- ~ e == R0 ->  (powerRZ e (Zplus n m)) == (Rmult (powerRZ e n) (powerRZ e m)).
-Intros e n m; Case n; Case m; Simpl; Auto with real.
-Intros n1 m1; Rewrite convert_add; Auto with real.
-Intros n1 m1; (CaseEqk '(compare m1 n1 EGAL)); Simpl; Auto with real.
+ ~ x == R0 ->  (powerRZ x (Zplus n m)) == (Rmult (powerRZ x n) (powerRZ x m)).
+Proof.
+Intro x; NewDestruct n as [|n1|n1]; NewDestruct m as [|m1|m1]; Simpl;
+  Auto with real.
+(* POS/POS *)
+Rewrite convert_add; 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 n1 m1); Auto with real.
-Rewrite (pow_RN_plus e (minus (convert n1) (convert m1)) (convert m1));
+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.
@@ -566,31 +609,33 @@ 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 m1 n1); Auto with real.
-Rewrite (pow_RN_plus e (minus (convert m1) (convert n1)) (convert n1));
+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 m1) (convert n1)).
+Change (gt (convert n1) (convert m1)).
 Apply compare_convert_SUPERIEUR; Auto.
-Intros n1 m1; (CaseEqk '(compare m1 n1 EGAL)); Simpl; Auto with real.
+(* 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 n1 m1); Auto with real.
-Rewrite (pow_RN_plus e (minus (convert n1) (convert m1)) (convert m1));
+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 m1 n1); Auto with real.
-Rewrite (pow_RN_plus e (minus (convert m1) (convert n1)) (convert n1));
+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 m1) (convert n1)).
+Change (gt (convert n1) (convert m1)).
 Apply compare_convert_SUPERIEUR; Auto.
-Intros n1 m1; Rewrite convert_add; Auto with real.
+(* NEG/NEG *)
+Rewrite convert_add; Auto with real.
 Intros H'; Rewrite pow_add; Auto with real.
 Apply Rinv_Rmult; Auto.
 Apply pow_nonzero; Auto.
@@ -601,6 +646,7 @@ Hints 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))
@@ -613,19 +659,22 @@ Intros m2; Rewrite bij1; Auto.
 Unfold Zpower_nat; Auto.
 Qed.
  
-Lemma powerRZ_lt: (e : R) (z : Z) (Rlt R0 e) ->  (Rlt R0 (powerRZ e z)).
-Intros e z; Case z; Simpl; Auto with real.
+Lemma powerRZ_lt: (x : R) (z : Z) (Rlt R0 x) ->  (Rlt R0 (powerRZ x z)).
+Proof.
+Intros x z; Case z; Simpl; Auto with real.
 Qed.
 Hints Resolve powerRZ_lt :real.
  
-Lemma powerRZ_le: (e : R) (z : Z) (Rlt R0 e) ->  (Rle R0 (powerRZ e z)).
-Intros e z H'; Apply Rlt_le; Auto with real.
+Lemma powerRZ_le: (x : R) (z : Z) (Rlt R0 x) ->  (Rle R0 (powerRZ x z)).
+Proof.
+Intros x z H'; Apply Rlt_le; Auto with real.
 Qed.
 Hints 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).
+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.
@@ -634,6 +683,7 @@ Intros p H'; Absurd `0 <= (NEG p)`;Auto with zarith.
 Qed.
 
 Lemma powerRZ_R1: (n : Z)  (powerRZ R1 n) == R1.
+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.
@@ -658,11 +708,11 @@ Definition sum_nat_f [s,n:nat;f:nat->nat]:nat:=
 
 (*********)
 Definition sum_nat_O [n:nat]:nat:=
-  (sum_nat_f_O [x]x n).
+  (sum_nat_f_O [x:nat]x n).
 
 (*********)
 Definition sum_nat [s,n:nat]:nat:=
-  (sum_nat_f s n [x]x).
+  (sum_nat_f s n [x:nat]x).
 
 (*******************************)
 (**            Sum             *)
@@ -682,6 +732,7 @@ 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).
@@ -692,6 +743,7 @@ 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
@@ -715,6 +767,7 @@ Definition R_dist:R->R->R:=[x,y:R](Rabsolu (Rminus x y)).
 
 (*********)
 Lemma R_dist_pos:(x,y:R)(Rge (R_dist x y) R0).
+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.
@@ -722,6 +775,7 @@ Qed.
 
 (*********)
 Lemma R_dist_sym:(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;
@@ -734,6 +788,7 @@ Qed.
 
 (*********)
 Lemma R_dist_refl:(x,y:R)((R_dist x y)==R0<->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).
@@ -744,12 +799,14 @@ Apply (eq_Rminus x y H).
 Qed.
 
 Lemma R_dist_eq:(x:R)(R_dist x x)==R0.
+Proof.
 Unfold R_dist;Intros;SplitAbsolu;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))).
+Proof.
 Intros;Unfold R_dist; Replace ``x-y`` with ``(x-z)+(z-y)``;
   [Apply (Rabsolu_triang ``x-z`` ``z-y``)|Ring].
 Qed.
@@ -757,6 +814,7 @@ 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))).
+Proof.
 Intros;Unfold R_dist;
  Replace (Rminus (Rplus a c) (Rplus b d))
   with (Rplus (Rminus a b) (Rminus c d)).