Ajouts de lemmes (pour Float)

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

5 files changed, 407 insertions, 29 deletions

diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index a6ac4c922..240b8c920 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -132,6 +132,20 @@ Generalize (Rgt_plus_plus_r (Ropp R1) (IZR (up r)) r H);Intro;
 Save.
 
 (**********)
+Lemma Int_part_INR:(n : nat)  (Int_part (INR n)) = (inject_nat n).
+Intros n; Unfold Int_part.
+Cut (up (INR n)) = (Zplus (inject_nat n) (inject_nat (1))).
+Intros H'; Rewrite H'; Simpl; Ring.
+Apply sym_equal; Apply tech_up; Auto.
+Replace (Zplus (inject_nat n) (inject_nat (1))) with (INZ (S n)).
+Repeat Rewrite <- INR_IZR_INZ.
+Apply lt_INR; Auto.
+Rewrite Zplus_sym; Rewrite <- inj_plus; Simpl; Auto.
+Rewrite plus_IZR; Simpl; Auto with real.
+Repeat Rewrite <- INR_IZR_INZ; Auto with real.
+Save.
+
+(**********)
 Lemma fp_nat:(r:R)(frac_part r)==R0->(Ex [c:Z](r==(IZR c))).
 Unfold frac_part;Intros;Split with (Int_part r);Apply Rminus_eq; Auto with zarith real.
 Save.
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 23fb79c5c..f2603ca67 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1208,18 +1208,18 @@ Save.
 Hints Resolve plus_INR minus_INR mult_INR : real.
 
 (*********)
-Lemma INR_lt_0:(n:nat)(lt O n)->``0 < (INR n)``.
+Lemma lt_INR_0:(n:nat)(lt O n)->``0 < (INR n)``.
 Induction 1; Intros; Auto with real.
 Rewrite S_INR; Auto with real.
 Save.
-Hints Resolve INR_lt_0: real.
+Hints Resolve lt_INR_0: real.
 
-Lemma INR_lt_nm:(n,m:nat)(lt n m)->``(INR n) < (INR m)``.
+Lemma lt_INR:(n,m:nat)(lt n m)->``(INR n) < (INR m)``.
 Induction 1; Intros; Auto with real.
 Rewrite S_INR; Auto with real.
 Rewrite S_INR; Apply Rlt_trans with (INR m0); Auto with real.
 Save.
-Hints Resolve INR_lt_nm: real.
+Hints Resolve lt_INR: real.
 
 Lemma INR_lt_1:(n:nat)(lt (S O) n)->``1 < (INR n)``.
 Intros;Replace ``1`` with (INR (S O));Auto with real.
@@ -1228,27 +1228,42 @@ Hints Resolve INR_lt_1: real.
 
 (**********)
 Lemma INR_pos : (p:positive)``0<(INR (convert p))``.
-Intro; Apply INR_lt_0.
+Intro; Apply lt_INR_0.
 Simpl; Auto with real.
 Apply compare_convert_O.
 Save.
 Hints Resolve INR_pos : real.
 
 (**********)
-Lemma INR_le:(n:nat)``0 <= (INR n)``.
+Lemma pos_INR:(n:nat)``0 <= (INR n)``.
 Intro n; Case n.
 Simpl; Auto with real.
 Auto with arith real.
 Save.
-Hints Resolve INR_le: real.
+Hints Resolve pos_INR: real.
+
+Lemma INR_lt:(n,m:nat)``(INR n) < (INR m)``->(lt n m).
+Double Induction 1 2;Intros.
+Simpl;ElimType False;Apply (Rlt_antirefl R0);Auto.
+Auto with arith.
+Generalize (pos_INR (S n0));Intro;Cut (INR O)==R0;
+  [Intro H2;Rewrite H2 in H0;Idtac|Simpl;Trivial]. 
+Generalize (Rle_lt_trans ``0`` (INR (S n0)) ``0`` H1 H0);Intro;
+  ElimType False;Apply (Rlt_antirefl R0);Auto.
+Do 2 Rewrite S_INR in H1;Cut ``(INR n1) < (INR n0)``.
+Intro H2;Generalize (H0 n0 H2);Intro;Auto with arith.
+Apply (Rlt_anti_compatibility ``1`` (INR n1) (INR n0)).
+Rewrite Rplus_sym;Rewrite (Rplus_sym ``1`` (INR n0));Trivial.
+Save.
+Hints Resolve INR_lt: real.
 
 (*********)
-Lemma INR_le_nm:(n,m:nat)(le n m)->``(INR n)<=(INR m)``.
+Lemma le_INR:(n,m:nat)(le n m)->``(INR n)<=(INR m)``.
 Induction 1; Intros; Auto with real.
 Rewrite S_INR.
 Apply Rle_trans with (INR m0); Auto with real.
 Save.
-Hints Resolve INR_le_nm: real.
+Hints Resolve le_INR: real.
 
 (**********)
 Lemma not_INR_O:(n:nat)``(INR n)<>0``->~n=O.
@@ -1276,6 +1291,27 @@ Apply sym_not_eqT; Apply imp_not_Req; Auto with real.
 Save.
 Hints Resolve not_nm_INR : real.
 
+Lemma INR_eq: (n,m:nat)(INR n)==(INR m)->n=m.
+Intros;Case (le_or_lt n m); Intros H1.
+Case (le_lt_or_eq ? ? H1); Intros H2;Auto.
+Cut ~n=m.
+Intro H3;Generalize (not_nm_INR n m H3);Intro H4;
+  ElimType False;Auto.
+Omega.
+Symmetry;Cut ~m=n.
+Intro H3;Generalize (not_nm_INR m n H3);Intro H4;
+  ElimType False;Auto.
+Omega.
+Save.
+Hints Resolve INR_eq : real.
+
+Lemma INR_le: (n, m : nat) (Rle (INR n) (INR m)) ->  (le n m).
+Intros;Elim H;Intro.
+Generalize (INR_lt n m H0);Intro;Auto with arith.
+Generalize (INR_eq n m H0);Intro;Rewrite H1;Auto.
+Save.
+Hints Resolve INR_le : real.
+
 Lemma not_1_INR:(n:nat)~n=(S O)->``(INR n)<>1``.
 Replace ``1``  with (INR (S O)); Auto with real.
 Save.
@@ -1299,8 +1335,8 @@ Induction n; Auto with real.
 Intros; Simpl; Rewrite bij1; Auto with real.
 Save.
 
-Lemma  plus_IZR_NEG_POS : 
-	(p,q:positive)(IZR `(POS p)+(NEG q)`)==``(IZR (POS p))+(IZR (NEG q))``.
+Lemma plus_IZR_NEG_POS : 
+  (p,q:positive)(IZR `(POS p)+(NEG q)`)==``(IZR (POS p))+(IZR (NEG q))``.
 Intros.
 Case (lt_eq_lt_dec (convert p) (convert q)).
 Intros [H | H]; Simpl.
@@ -1327,6 +1363,20 @@ Simpl; Intros; Rewrite convert_add; Rewrite plus_INR; Auto with real.
 Save.
 
 (**********)
+Lemma mult_IZR:(z,t:Z)(IZR `z*t`)==``(IZR z)*(IZR t)``.
+Intros z t; Case z; Case t; Simpl; Auto with real.
+Intros t1 z1; Rewrite times_convert; Auto with real.
+Intros t1 z1; Rewrite times_convert; Auto with real.
+Rewrite Rmult_sym.
+Rewrite Ropp_mul1; Auto with real.
+Apply eq_Ropp; Rewrite mult_sym; Auto with real.
+Intros t1 z1; Rewrite times_convert; Auto with real.
+Rewrite Ropp_mul1; Auto with real.
+Intros t1 z1; Rewrite times_convert; Auto with real.
+Rewrite Ropp_mul2; Auto with real.
+Save.
+
+(**********)
 Lemma Ropp_Ropp_IZR:(z:Z)(IZR (`-z`))==``-(IZR z)``.
 Intro z; Case z; Simpl; Auto with real.
 Save.
@@ -1368,6 +1418,12 @@ Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H);
  Intro;Omega.
 Save.
 
+(**********)
+Lemma not_O_IZR:(z:Z)`z<>0`->``(IZR z)<>0``.
+Intros z H; Red; Intros H0; Case H.
+Apply eq_IZR; Auto.
+Save.
+
 (*********)
 Lemma le_O_IZR:(z:Z)``0<= (IZR z)``->`0<=z`.
 Unfold Rle; Intros z [H|H].
@@ -1395,6 +1451,17 @@ Intros;Apply Rlt_not_ge;Red;Intro.
 Generalize (lt_IZR m n H0); Intro; Omega.
 Save.
 
+Lemma IZR_le: (m,n:Z) `m<= n` -> ``(IZR m)<=(IZR n)``.
+Intros;Apply Rgt_not_le;Red;Intro.
+Unfold Rgt in H0;Generalize (lt_IZR n m H0); Intro; Omega.
+Save.
+
+Lemma IZR_lt: (m,n:Z) `m< n` -> ``(IZR m)<(IZR n)``.
+Intros;Cut `m<=n`.
+Intro H0;Elim (IZR_le m n H0);Intro;Auto.
+Generalize (eq_IZR m n H1);Intro;ElimType False;Omega.
+Omega.
+
 Lemma one_IZR_lt1 : (z:Z)``-1<(IZR z)<1``->`z=0`.
 Intros z (H1,H2).
 Apply Zle_antisym.
@@ -1419,9 +1486,9 @@ Save.
 
 
 (**********)
-Lemma single_z_r_R1
-  : (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->``(IZR x)<=r+1``
-    ->z=x.
+Lemma single_z_r_R1: 
+   (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->
+        ``(IZR x)<=r+1``->z=x.
 Intros; Apply one_IZR_r_R1 with r; Auto.
 Save.
 
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 1079323dc..34bb1f790 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -76,6 +76,35 @@ Generalize (not_Rle r1 r2 n);Clear n;Intro;Unfold Rgt in H0;
  Apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)).
 Save.
 
+Lemma RmaxLess1: (r1, r2 : R)  (Rle r1 (Rmax r1 r2)).
+Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real.
+Save.
+ 
+Lemma RmaxLess2: (r1, r2 : R)  (Rle r2 (Rmax r1 r2)).
+Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real.
+Save.
+ 
+Lemma RmaxSym: (p, q : R)  (Rmax p q) == (Rmax q p).
+Intros p q; Unfold Rmax;
+ Case (total_order_Rle p q); Case (total_order_Rle q p); Auto; Intros H1 H2;
+ Apply Rle_antisym; Auto with real.
+Save.
+
+Lemma RmaxRmult:
+ (p, q, r : R)
+ (Rle R0 r) ->  (Rmax (Rmult r p) (Rmult r q)) == (Rmult r (Rmax p q)).
+Intros p q r H; Unfold Rmax.
+Case (total_order_Rle p q); Case (total_order_Rle (Rmult r p) (Rmult r q));
+ Auto; Intros H1 H2; Auto.
+Case H; Intros E1.
+Case H1; Auto with real.
+Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto.
+Case H; Intros E1.
+Case H2; Auto with real.
+Apply Rle_monotony_contra with z := r; Auto.
+Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto.
+Save.
+
 (*******************************)
 (*           Rabsolu           *)
 (*******************************)
@@ -127,6 +156,12 @@ Assumption.
 Trivial.
 Save.
 
+Lemma Rabsolu_left1: (a : R) (Rle a R0) ->  (Rabsolu a) == (Ropp a).
+Intros a H; Case H; Intros H1.
+Apply Rabsolu_left; Auto.
+Rewrite H1; Simpl; Rewrite Rabsolu_right; Auto with real.
+Save.
+
 (*********)
 Lemma Rabsolu_pos:(x:R)(Rle R0 (Rabsolu x)).
 Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro.
@@ -262,7 +297,6 @@ Intro;Generalize (Rle_not R1 R0 Rlt_R0_R1);Intro;
 Ring.
 Save.
 
-
 (*********)
 Lemma Rabsolu_triang:(a,b:R)(Rle (Rabsolu (Rplus a b)) 
                                 (Rplus (Rabsolu a) (Rabsolu b))).
@@ -366,3 +400,36 @@ Fold (Rgt a x) in H;Generalize (Rgt_ge_trans a x R0 H r);Intro;
  Assumption.
 Save.
 
+Lemma RmaxAbs:
+ (p, q, r : R)
+ (Rle p q) -> (Rle q r) ->  (Rle (Rabsolu q) (Rmax (Rabsolu p) (Rabsolu r))).
+Intros p q r H' H'0; Case (Rle_or_lt R0 p); Intros H'1.
+Repeat Rewrite Rabsolu_right; Auto with real.
+Apply Rle_trans with r; Auto with real.
+Apply RmaxLess2; Auto.
+Apply Rge_trans with p; Auto with real; Apply Rge_trans with q; Auto with real.
+Apply Rge_trans with p; Auto with real.
+Rewrite (Rabsolu_left p); Auto.
+Case (Rle_or_lt R0 q); Intros H'2.
+Repeat Rewrite Rabsolu_right; Auto with real.
+Apply Rle_trans with r; Auto.
+Apply RmaxLess2; Auto.
+Apply Rge_trans with q; Auto with real.
+Rewrite (Rabsolu_left q); Auto.
+Case (Rle_or_lt R0 r); Intros H'3.
+Repeat Rewrite Rabsolu_right; Auto with real.
+Apply Rle_trans with (Ropp p); Auto with real.
+Apply RmaxLess1; Auto.
+Rewrite (Rabsolu_left r); Auto.
+Apply Rle_trans with (Ropp p); Auto with real.
+Apply RmaxLess1; Auto.
+Save.
+
+Lemma Rabsolu_Zabs: (z : Z)  (Rabsolu (IZR z)) == (IZR (Zabs z)).
+Intros z; Case z; Simpl; Auto with real.
+Apply Rabsolu_right; Auto with real.
+Intros p0; Apply Rabsolu_right; Auto with real zarith.
+Intros p0; Rewrite Rabsolu_Ropp.
+Apply Rabsolu_right; Auto with real zarith.
+Save.
+ 
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 857969b74..3885ce173 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i Some properties about pow and sum have been made with John Harrison i*)
+(*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
 (*********************************************************)
 (*           Definition of the some functions            *)
 (*                                                       *)
@@ -16,6 +17,7 @@
 
 Require Export Rlimit.
 Require Omega.
+Require Import Zpower.
 
 (*******************************)
 (*      Factorial              *)
@@ -70,6 +72,81 @@ Fixpoint pow [r:R;n:nat]:R:=
     |(S n) => (Rmult r (pow r n))
   end.
 
+Theorem pow_O: (e : R)  (pow e O) == R1.
+Simpl; Auto with real.
+Qed.
+ 
+Theorem pow_1: (e : R)  (pow e (1)) == e.
+Simpl; Auto with real.
+Qed.
+ 
+Theorem 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.
+Intros n0 H' m; Rewrite H'; Auto with real.
+Qed.
+
+Lemma pow_nonzero:
+  (x:R) (n:nat) ~(x==R0) -> ~((pow x n)==R0).
+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.
+Save.
+
+Hints Resolve pow_O pow_1 pow_add pow_nonzero:real.
+ 
+Theorem pow_RN_plus:
+ (e : 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.
+Intros n0 H' m H'0.
+Rewrite Rmult_assoc; Rewrite <- H'; Auto.
+Qed.
+
+Theorem 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.
+Qed.
+Hints Resolve pow_lt :real.
+
+Theorem 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.
+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_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.
+
+Theorem 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).
+Rewrite pow_add.
+Pattern 1 (pow e n); Replace (pow e n) with (Rmult R1 (pow e 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.
+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 tech_pow_Rmult:(x:R)(n:nat)(Rmult x (pow x n))==(pow x (S n)).
 Induction n; Simpl; Trivial.
@@ -107,7 +184,7 @@ Intro;Rewrite H1;Pattern 1 (Rplus R1 (Rmult (INR (S n0)) e));
 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) 
-        (INR_lt_0 (S n1) (lt_O_Sn n1)));Fold (Rgt e R0) in H;
+        (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))).
 Rewrite (S_INR n0);Ring.
@@ -213,15 +290,6 @@ Intros;Elim H;Reflexivity.
 Intros; Simpl;Apply Rmult_Ol.
 Save.
 
-Lemma pow_nonzero:
-  (x:R) (n:nat) ~(x==R0) -> ~((pow x n)==R0).
-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.
-Save.
-
 Lemma Rinv_pow:
   (x:R) (n:nat) ~(x==R0) -> (Rinv (pow x n))==(pow (Rinv x) n).
 Intros; Elim n; Simpl.
@@ -286,6 +354,168 @@ Assumption.
 Red;Intro; Apply R1_neq_R0;Assumption.
 Save.
 
+Theorem pow_R1:
+ (r : R) (n : nat) (pow r n) == R1 ->  (Rabsolu r) == R1 \/ n = O.
+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 Power_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 Power_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.
+
+(*******************************)
+(*          PowerRZ            *)
+(*******************************)
+(*i Due to L.Thery i*)
+
+Tactic Definition CaseEqk name :=
+Generalize (refl_equal ? name); Pattern -1 name; Case name.
+
+Definition powerRZ :=
+   [e : R] [n : Z]  Cases n of
+                      ZERO => R1
+                     | (POS p) => (pow e (convert p))
+                     | (NEG p) => (Rinv (pow e (convert p)))
+                    end.
+
+Theorem 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.
+Qed.
+
+Theorem powerRZ_O: (e : R)  (powerRZ e ZERO) == R1.
+Simpl; Auto.
+Qed.
+ 
+Theorem powerRZ_1: (e : R)  (powerRZ e (Zs ZERO)) == e.
+Simpl; Auto with real.
+Qed.
+ 
+Theorem powerRZ_NOR: (e : R) (z : Z) ~ e == R0 ->  ~ (powerRZ e z) == R0.
+Intros e z; Case z; Simpl; Auto with real.
+Qed.
+Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR :real.
+ 
+Theorem powerRZ_add:
+ (e : 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.
+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));
+ 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 m1 n1); Auto with real.
+Rewrite (pow_RN_plus e (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.
+Change (gt (convert m1) (convert n1)).
+Apply compare_convert_SUPERIEUR; Auto.
+Intros n1 m1; (CaseEqk '(compare m1 n1 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));
+ 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));
+ 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)).
+Apply compare_convert_SUPERIEUR; Auto.
+Intros n1 m1; 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.
+Qed.
+Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add :real.
+ 
+Theorem Zpower_nat_powerRZ:
+ (n, m : nat)
+  (IZR (Zpower_nat (inject_nat n) m)) == (powerRZ (INR n) (inject_nat m)).
+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.
+Qed.
+ 
+Theorem powerRZ_lt: (e : R) (z : Z) (Rlt R0 e) ->  (Rlt R0 (powerRZ e z)).
+Intros e z; Case z; Simpl; Auto with real.
+Qed.
+Hints Resolve powerRZ_lt :real.
+ 
+Theorem powerRZ_le: (e : R) (z : Z) (Rlt R0 e) ->  (Rle R0 (powerRZ e z)).
+Intros e z H'; Apply Rlt_le; Auto with real.
+Qed.
+Hints Resolve powerRZ_le :real.
+ 
+Theorem Zpower_nat_powerRZ_absolu:
+ (n, m : Z)
+ (Zle ZERO m) ->  (IZR (Zpower_nat n (absolu m))) == (powerRZ (IZR n) m).
+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.
+Qed.
+
+Theorem powerRZ_R1: (n : Z)  (powerRZ R1 n) == R1.
+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.
+Qed.
+
 (*******************************)
 (*  Sum of n first naturals    *)
 (*******************************)
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index 1d59a71e3..2bc5063eb 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -31,7 +31,7 @@ Split with O;Intros;Rewrite (simpl_fact n);Unfold R_dist;
 Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))).
 Cut (Rlt (Rminus (Rinv eps) R1) R0).
 Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) R0 (INR n) H2 
-   (INR_le n));Clear H2;Intro;
+   (pos_INR n));Clear H2;Intro;
  Unfold Rminus in H2;Generalize (Rlt_compatibility R1 
        (Rplus (Rinv eps) (Ropp R1)) (INR n) H2);
  Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps);
@@ -54,7 +54,7 @@ Apply Rlt_minus;Unfold Rgt in a;Rewrite <- Rinv_R1;
  Apply (Rinv_lt R1 eps);Auto;
  Rewrite (let (H1,H2)=(Rmult_ne eps) in H2);Unfold Rgt in H;Assumption.
 Unfold Rgt in H1;Apply Rlt_le;Assumption.
-Unfold Rgt;Apply Rlt_Rinv; Apply INR_lt_0;Apply lt_O_Sn.
+Unfold Rgt;Apply Rlt_Rinv; Apply lt_INR_0;Apply lt_O_Sn.
 (**)
 Cut `0<=(up (Rminus (Rinv eps) R1))`.
 Intro;Elim (IZN (up (Rminus (Rinv eps) R1)) H0);Intros;
@@ -65,7 +65,7 @@ Intro;Elim (IZN (up (Rminus (Rinv eps) R1)) H0);Intros;
 Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))).
 Cut (Rlt (Rminus (Rinv eps) R1) (INR x)).
 Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) (INR x) (INR n) 
-      H4 (INR_le_nm x n ([n,m:nat; H:(ge m n)]H x n H2)));  
+      H4 (le_INR x n ([n,m:nat; H:(ge m n)]H x n H2)));  
  Clear H4;Intro;Unfold Rminus in H4;Generalize (Rlt_compatibility R1 
        (Rplus (Rinv eps) (Ropp R1)) (INR n) H4);
  Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps);
@@ -89,7 +89,7 @@ Cut (IZR (up (Rminus (Rinv eps) R1)))==(IZR (INZ x));
 Elim (archimed (Rminus (Rinv eps) R1));Intros;Clear H6;
  Unfold Rgt in H5;Rewrite H4 in H5;Rewrite INR_IZR_INZ;Assumption.
 Unfold Rgt in H1;Apply Rlt_le;Assumption.
-Unfold Rgt;Apply Rlt_Rinv; Apply INR_lt_0;Apply lt_O_Sn.
+Unfold Rgt;Apply Rlt_Rinv; Apply lt_INR_0;Apply lt_O_Sn.
 Apply (le_O_IZR (up (Rminus (Rinv eps) R1))); 
  Apply (Rle_trans R0 (Rminus (Rinv eps) R1) 
   (IZR (up (Rminus (Rinv eps) R1)))).