ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contrib/omega vers theories/ZArith

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

6 files changed, 1093 insertions, 0 deletions

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 65571855e..593555586 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -84,6 +84,15 @@ Intros Hn; Elim Hn; Intros.
 Rewrite -> H1; Apply H.
 Save.
 
+Lemma inject_nat_set :
+  (P:Z->Set)((n:nat)(P (inject_nat n))) -> 
+    (x:Z) `0 <= x` -> (P x).
+Intros.
+Specialize (inject_nat_complete_inf x H0).
+Intros Hn; Elim Hn; Intros.
+Rewrite -> p; Apply H.
+Save.
+
 Lemma ZERO_le_inj :
   (n:nat) `0 <= (inject_nat n)`.
 Induction n; Simpl; Intros;
@@ -102,6 +111,17 @@ Intros; Apply inject_nat_prop;
 | Assumption].
 Save.
 
+Lemma natlike_rec : (P:Z->Set) (P `0`) ->
+  ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) ->
+  (x:Z) `0 <= x` -> (P x).
+Intros; Apply inject_nat_set;
+[ Induction n;
+  [ Simpl; Assumption
+  | Intros; Rewrite -> (inj_S n0);
+    Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ]
+| Assumption].
+Save.
+
 Lemma Z_lt_induction : 
   (P:Z->Prop)
      ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x))
@@ -131,3 +151,33 @@ Apply Zgt_S_le. Apply Zlt_gt. Intuition.
 
 Assumption.
 Save.
+
+Lemma Z_lt_rec : 
+  (P:Z->Set)
+     ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x))
+  -> (x:Z)`0 <= x`->(P x).
+Proof.
+Intros P H x Hx.
+Cut (x:Z)`0 <= x`->(y:Z)`0 <= y < x`->(P y).
+Intro.
+Apply (H0 (Zs x)).
+Auto with zarith.
+
+Split; [ Assumption | Exact (Zlt_n_Sn x) ].
+
+Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_rec.
+Intros.
+Absurd `0 <= 0`; Try Assumption.
+Apply Zgt_not_le.
+Apply Zgt_le_trans with m:=y.
+Apply Zlt_gt.
+Intuition. Intuition.
+
+Intros. Apply H. Intros.
+Apply (H1 H0).
+Split; [ Intuition | Idtac ].
+Apply Zlt_le_trans with y. Intuition.
+Apply Zgt_S_le. Apply Zlt_gt. Intuition.
+
+Assumption.
+Save.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
new file mode 100644
index 000000000..69ce3b6f8
--- /dev/null
+++ b/theories/ZArith/Zcomplements.v
@@ -0,0 +1,359 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require ZArith.
+Require Omega.
+Require Wf_nat.
+
+(* Multiplication by a number >0 preserves Zcompare. It also perserves
+  Zle, Zlt, Zge, Zgt *)
+
+Implicit Arguments On.
+
+Lemma Zmult_zero : (x,y:Z)`x*y=0` -> `x=0` \/ `y=0`.
+NewDestruct x; NewDestruct y; Auto.
+Simpl; Intros; Discriminate H.
+Simpl; Intros; Discriminate H.
+Simpl; Intros; Discriminate H.
+Simpl; Intros; Discriminate H.
+Save.
+
+Lemma Zeq_Zminus : (x,y:Z)x=y -> `x-y = 0`.
+Intros; Omega.
+Save.
+
+Lemma Zminus_Zeq : (x,y:Z)`x-y=0` -> x=y.
+Intros; Omega.
+Save.
+
+Lemma Zmult_Zminus_distr_l : (x,y,z:Z)`(x-y)*z = x*z - y*z`.
+Intros; Unfold Zminus.
+Rewrite <- Zopp_Zmult.
+Apply Zmult_plus_distr_l.
+Save.
+
+Lemma  Zmult_Zminus_distr_r : (x,y,z:Z)`z*(x-y) = z*x - z*y`.
+Intros; Rewrite (Zmult_sym z `x-y`).
+Rewrite (Zmult_sym  z x).
+Rewrite (Zmult_sym z y).
+Apply Zmult_Zminus_distr_l.
+Save.
+
+Lemma Zmult_reg_left : (x,y,z:Z)`z>0` -> `z*x=z*y` -> x=y.
+Intros.
+Generalize (Zeq_Zminus H0).
+Intro.
+Apply Zminus_Zeq.
+Rewrite <- (Zmult_Zminus_distr_r x y z) in H1. 
+Elim (Zmult_zero H1).
+Omega.
+Trivial.
+Save.
+
+Lemma Zmult_reg_right : (x,y,z:Z)`z>0` -> `x*z=y*z` -> x=y.
+Intros x y z Hz.
+Rewrite (Zmult_sym x z).
+Rewrite (Zmult_sym y z).
+Intro; Apply Zmult_reg_left with z; Assumption.
+Save.
+    
+Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`.
+Intro; Unfold Zpred; Omega.
+Save.
+
+Lemma Zlt_Zplus : 
+  (x1,x2,y1,y2:Z)`x1 < x2` -> `y1 < y2` -> `x1 + y1 < x2 + y2`.
+Intros; Omega.
+Save.
+
+Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`.
+
+Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro;
+Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`;
+[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption
+| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r);
+  Repeat Rewrite Zmult_n_1;
+  Intro; Apply Zlt_Zplus; Assumption
+| Assumption ].
+Save.
+
+Lemma Zlt_Zmult_right2 : (x,y,z:Z)`z>0`  -> `x*z < y*z` -> `x < y`.
+Intros x y z H; Rewrite (Zs_pred z).
+Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`->`x < y`.
+Simpl; Do 2 Rewrite Zmult_n_1; Auto 1.
+Unfold Zs.
+Intros x0 Hx0; Repeat Rewrite Zmult_plus_distr_r.
+Repeat Rewrite Zmult_n_1.
+Omega. (* Auto with zarith. *)
+Unfold Zpred; Omega.
+Save.
+
+Lemma Zle_Zmult_right : (x,y,z:Z)`z>0` -> `x <= y` -> `x*z <= y*z`.
+Intros x y z Hz Hxy.
+Elim (Zle_lt_or_eq x y Hxy).
+Intros; Apply Zlt_le_weak.
+Apply Zlt_Zmult_right; Trivial.
+Intros; Apply Zle_refl.
+Rewrite H; Trivial.
+Save.
+
+Lemma Zle_Zmult_right2 :  (x,y,z:Z)`z>0` -> `x*z <= y*z` -> `x <= y`.
+Intros x y z Hz Hxy.
+Elim (Zle_lt_or_eq `x*z` `y*z` Hxy).
+Intros; Apply Zlt_le_weak.
+Apply Zlt_Zmult_right2 with z; Trivial.
+Intros; Apply Zle_refl.
+Apply Zmult_reg_right with z; Trivial.
+Save.
+
+Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`.
+
+Intros; Apply Zlt_gt; Apply Zlt_Zmult_right; 
+[ Assumption | Apply Zgt_lt ; Assumption ].
+Save.
+
+Lemma Zlt_Zmult_left : (x,y,z:Z)`z>0` -> `x < y` -> `z*x < z*y`.
+
+Intros;
+Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y);
+Apply Zlt_Zmult_right; Assumption.
+Save.
+
+Lemma Zgt_Zmult_left : (x,y,z:Z)`z>0` -> `x > y` -> `z*x > z*y`.
+Intros;
+Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y);
+Apply Zgt_Zmult_right; Assumption.
+Save.
+
+Theorem Zcompare_Zmult_right : (x,y,z:Z)` z>0` -> `x ?= y`=`x*z ?= y*z`.
+
+Intros; Apply Zcompare_egal_dec;
+[ Intros; Apply Zlt_Zmult_right; Trivial
+| Intro Hxy; Apply [a,b:Z](let (t1,t2)=(Zcompare_EGAL a b) in t2);
+  Rewrite ((let (t1,t2)=(Zcompare_EGAL x y) in t1) Hxy); Trivial
+| Intros; Apply Zgt_Zmult_right; Trivial
+].
+Save.
+
+Theorem  Zcompare_Zmult_left : (x,y,z:Z)`z>0` -> `x ?= y`=`z*x ?= z*y`.
+Intros;
+Rewrite (Zmult_sym z x);
+Rewrite (Zmult_sym z y);
+Apply Zcompare_Zmult_right; Assumption.
+Save.
+
+
+Section diveucl.
+
+Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. 
+NewDestruct x.
+Left ; Split with ZERO; Reflexivity.
+
+NewDestruct p.
+Right ; Split with (POS p); Reflexivity.
+
+Left ; Split with (POS p); Reflexivity.
+
+Right ; Split with ZERO; Reflexivity.
+
+NewDestruct p.
+Right ; Split with (NEG (add xH p)).
+Rewrite NEG_xI.
+Rewrite NEG_add.
+Omega.
+
+Left ; Split with (NEG p); Reflexivity.
+
+Right ; Split with `-1`; Reflexivity.
+Save.
+
+(* The biggest power of 2 that is stricly less than a *)
+(* Easy to compute : replace all "1" of the binary representation by
+   "0", except the first "1" (or the first one :-) *)
+Fixpoint floor_pos [a : positive] : positive :=
+  Cases a of
+  | xH => xH
+  | (xO a') => (xO (floor_pos a'))
+  | (xI b') => (xO (floor_pos b'))
+  end.
+
+Definition floor := [a:positive](POS (floor_pos a)).
+
+Lemma floor_gt0 : (x:positive) `(floor x) > 0`.
+Intro.
+Compute.
+Trivial.
+Save.
+
+Lemma floor_ok : (a:positive) 
+  `(floor a) <=  (POS a) < 2*(floor a)`. 
+Unfold floor.
+Induction a.
+
+Intro p; Simpl.
+Repeat Rewrite POS_xI.
+Rewrite (POS_xO (xO (floor_pos p))). 
+Rewrite (POS_xO (floor_pos p)).
+Omega.
+
+Intro p; Simpl.
+Repeat Rewrite POS_xI.
+Rewrite (POS_xO (xO (floor_pos p))).
+Rewrite (POS_xO (floor_pos p)).
+Rewrite (POS_xO p).
+Omega.
+
+Simpl; Omega.
+Save.
+
+Lemma Zdiv_eucl_POS : (b:Z)`b > 0` -> (p:positive)
+  { qr:Z*Z | let (q,r)=qr in `(POS p)=b*q+r` /\ `0 <= r < b` }.
+
+Induction p.
+
+(* p => (xI p) *)
+(* Notez l'utilisation des nouveaux patterns Intro *)
+Intros p' ((q,r), (Hrec1, Hrec2)).
+Elim (Z_lt_ge_dec `2*r+1` b); 
+[ Exists `(2*q, 2*r+1)`;
+  Rewrite POS_xI;
+  Rewrite Hrec1;
+  Split; 
+  [ Rewrite Zmult_Zplus_distr; 
+    Rewrite Zplus_assoc_l;
+    Rewrite (Zmult_permute b `2`);
+    Reflexivity
+  | Omega ]
+| Exists `(2*q+1, 2*r+1-b)`;
+  Rewrite POS_xI;
+  Rewrite Hrec1;
+  Split; 
+  [ Do 2 Rewrite Zmult_Zplus_distr; 
+    Unfold Zminus;
+    Do 2 Rewrite Zplus_assoc_l;
+    Rewrite <- (Zmult_permute `2` b);
+    Generalize `b*q`; Intros; Omega
+  | Omega ]
+].
+
+(* p => (xO p) *)
+Intros p' ((q,r), (Hrec1, Hrec2)).
+Elim (Z_lt_ge_dec `2*r` b); 
+[ Exists `(2*q,2*r)`;
+  Rewrite POS_xO;
+  Rewrite Hrec1;
+  Split; 
+  [ Rewrite Zmult_Zplus_distr; 
+    Rewrite (Zmult_permute b `2`);
+    Reflexivity
+  | Omega ]
+| Exists `(2*q+1, 2*r-b)`;
+  Rewrite POS_xO;
+  Rewrite Hrec1;
+  Split; 
+  [ Do 2 Rewrite Zmult_Zplus_distr; 
+    Unfold Zminus;
+    Rewrite <- (Zmult_permute `2` b);
+    Generalize `b*q`; Intros; Omega
+  | Omega ]
+].
+(* xH *)
+Elim (Z_le_gt_dec `2` b);
+[ Exists `(0,1)`; Omega
+| Exists `(1,0)`; Omega 
+].
+Save.
+
+Theorem Zdiv_eucl : (b:Z)`b > 0` -> (a:Z)
+  { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }.
+NewDestruct a;
+
+[ (* a=0 *) Exists `(0,0)`; Omega
+| (* a = (POS p) *) Intros; Apply Zdiv_eucl_POS; Auto
+| (* a = (NEG p) *) Intros; Elim (Zdiv_eucl_POS H p);
+  Intros (q,r) (Hp1, Hp2);
+  Elim (Z_le_gt_dec r `0`); 
+  [ Exists `(-q,0)`; Split;
+    [ Apply Zopp_intro; Simpl; Rewrite Hp1;
+      Rewrite Zero_right; 
+      Rewrite <- Zopp_Zmult;
+      Rewrite Zmult_Zopp_Zopp;
+      Generalize `b*q`; Intro; Omega 
+    | Omega
+    ]
+  | Exists `(-(q+1),b-r)`; Split;
+    [ Apply Zopp_intro;
+      Unfold Zminus; Simpl; Rewrite Hp1;
+      Repeat Rewrite Zopp_Zplus;
+      Repeat Rewrite <- Zopp_Zmult;
+      Rewrite Zmult_Zplus_distr;
+      Rewrite Zmult_Zopp_Zopp;
+      Rewrite Zplus_assoc_r;
+      Apply f_equal with f:=[c:Z]`b*q+c`;
+      Omega
+    | Omega ]
+  ]
+].
+Save.
+
+Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z)
+  { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }.
+Proof.
+Intros b Hb a.
+Elim (Z_le_gt_dec `0` b);Intro Hb'.
+Cut `b>0`;[Intro Hb''|Omega].
+Rewrite Zabs_eq;[Apply Zdiv_eucl;Assumption|Assumption].
+Cut `-b>0`;[Intro Hb''|Omega].
+Elim (Zdiv_eucl Hb'' a);Intros qr.
+Elim qr;Intros q r Hqr.
+Exists (pair ? ? `-q` r).
+Elim Hqr;Intros.
+Split.
+Rewrite <- Zmult_Zopp_left;Assumption.
+Rewrite Zabs_non_eq;[Assumption|Omega].
+Save.
+
+End diveucl.
+
+(* Two more induction principles upon Z. *)
+
+Theorem Z_lt_abs_rec : (P: Z -> Set)
+  ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p).
+Intros P HP p.
+LetTac Q:=[z]`0<=z`->(P z)*(P `-z`).
+Cut (Q `|p|`);[Intros|Apply (Z_lt_rec Q);Auto with zarith].
+Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith.
+Unfold Q;Clear Q;Intros.
+Apply pair;Apply HP.
+Rewrite Zabs_eq;Auto;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Rewrite Zabs_non_eq;Auto with zarith.
+Rewrite Zopp_Zopp;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Qed.
+
+Theorem Z_lt_abs_induction : (P: Z -> Prop)
+  ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p).
+Intros P HP p.
+LetTac Q:=[z]`0<=z`->(P z) /\ (P `-z`).
+Cut (Q `|p|`);[Intros|Apply (Z_lt_induction Q);Auto with zarith].
+Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith.
+Unfold Q;Clear Q;Intros.
+Split;Apply HP.
+Rewrite Zabs_eq;Auto;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Rewrite Zabs_non_eq;Auto with zarith.
+Rewrite Zopp_Zopp;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Qed.
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index d54d1a0a2..19f71b322 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -69,6 +69,7 @@ Hints Resolve
   Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *)
   Zle_reg_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *)
   Zle_reg_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *)
+  Zabs_pos (* :(x:Z)`0 <= |x|` *)
   
   (* B) Irreversible simplification lemmas : Probably to be declared as *)
   (* hints, when no other simplification is possible *)
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
new file mode 100644
index 000000000..45ad93aba
--- /dev/null
+++ b/theories/ZArith/Zlogarithm.v
@@ -0,0 +1,264 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(****************************************************************************)
+(*  The integer logarithms with base 2. There are three logarithms,	    *)
+(*    depending on the rounding of the real 2-based logarithm : 	    *)
+(*									    *)
+(*  Log_inf : y = (Log_inf x) iff 2^y <= x < 2^(y+1)			    *)
+(*  Log_sup : y = (Log_sup x) iff 2^(y-1) < x <= 2^y			    *)
+(*  Log_nearest : y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)	    *)
+(*									    *)
+(*  (Log_inf x) is the biggest integer that is smaller than (Log x)	    *)
+(*  (Log_inf x) is the smallest integer that is bigger than (Log x)	    *)
+(*  (Log_nearest x) is the integer nearest from (Log x). 		    *)
+(****************************************************************************)
+
+Require ZArith.
+Require Omega.
+Require Zcomplements.
+Require Zpower.
+
+Section Log_pos. (* Log of positive integers *)
+
+(* First we build log_inf and log_sup *)
+
+Fixpoint log_inf [p:positive] : Z :=  
+  Cases p of
+    xH => `0`	 				(* 1 *)
+  | (xO q) => (Zs (log_inf q))		(* 2n *)
+  | (xI q) => (Zs (log_inf q))		(* 2n+1 *)
+  end.
+Fixpoint log_sup [p:positive] : Z :=
+  Cases p of
+    xH => `0`					(* 1 *)
+  | (xO n) => (Zs (log_sup n)) 		(* 2n *)
+  | (xI n) => (Zs (Zs (log_inf n)))		(* 2n+1 *)
+  end.
+
+Hints Unfold log_inf log_sup.
+
+(* Then we give the specifications of log_inf and log_sup 
+  and prove their validity *)
+
+(* Hints Resolve ZERO_le_S : zarith. *)
+Hints Resolve Zle_trans : zarith.
+
+Theorem log_inf_correct : (x:positive) ` 0 <= (log_inf x)` /\
+  ` (two_p (log_inf x)) <= (POS x) < (two_p (Zs (log_inf x)))`.
+Induction x; Intros; Simpl;
+[ Elim H; Intros Hp HR; Clear H; Split;
+  [ Auto with zarith
+  | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp));
+    Rewrite (two_p_S (log_inf p) Hp);
+    Rewrite (two_p_S (log_inf p) Hp) in HR;
+    Rewrite (POS_xI p); Omega ]
+| Elim H; Intros Hp HR; Clear H; Split;
+  [ Auto with zarith
+  | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp));
+    Rewrite (two_p_S (log_inf p) Hp);
+    Rewrite (two_p_S (log_inf p) Hp) in HR;
+    Rewrite (POS_xO p); Omega ]
+| Unfold two_power_pos; Unfold shift_pos; Simpl; Omega 
+].
+Save.
+
+Definition log_inf_correct1 :=
+	[p:positive](proj1 ? ? (log_inf_correct p)).
+Definition log_inf_correct2 := 
+	[p:positive](proj2 ? ? (log_inf_correct p)).
+
+Opaque log_inf_correct1 log_inf_correct2.
+
+Hints Resolve log_inf_correct1 log_inf_correct2 : zarith.
+
+Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`.
+Induction p; Intros; Simpl; Auto with zarith.
+Save.
+
+(* For every p, either p is a power of two and (log_inf p)=(log_sup p)
+  either (log_sup p)=(log_inf p)+1 *)
+
+Theorem log_sup_log_inf : (p:positive)
+  either (POS p)=(two_p (log_inf p)) 
+  and_then (POS p)=(two_p (log_sup p))
+  or_else ` (log_sup p)=(Zs (log_inf p))`.
+
+Induction p; Intros;
+[ Elim H; Right; Simpl;
+  Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
+  Rewrite POS_xI; Unfold Zs; Omega
+| Elim H; Clear H; Intro Hif;
+  [ Left; Simpl;
+    Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
+    Rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0));
+    Rewrite <- (proj1 ? ? Hif); Rewrite <- (proj2 ? ? Hif);
+    Auto
+  | Right; Simpl;
+    Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
+    Rewrite POS_xO; Unfold Zs; Omega ]
+| Left; Auto ].
+Save.
+
+Theorem log_sup_correct2 : (x:positive)
+  ` (two_p (Zpred (log_sup x))) < (POS x) <= (two_p (log_sup x))`.
+
+Intro.
+Elim (log_sup_log_inf x).
+(* x is a power of two and log_sup = log_inf *)
+Intros (E1,E2); Rewrite E2.
+Split ; [ Apply two_p_pred; Apply log_sup_correct1 | Apply Zle_n ].
+Intros (E1,E2); Rewrite E2.
+Rewrite <- (Zpred_Sn (log_inf x)).
+Generalize (log_inf_correct2 x); Omega.
+Save.
+
+Lemma log_inf_le_log_sup : 
+	(p:positive) `(log_inf p) <= (log_sup p)`.
+Induction p; Simpl; Intros; Omega.
+Save.
+
+Lemma log_sup_le_Slog_inf : 
+	(p:positive) `(log_sup p) <= (Zs (log_inf p))`.
+Induction p; Simpl; Intros; Omega.
+Save.
+
+(* Now it's possible to specify and build the Log rounded to the nearest *)
+
+Fixpoint log_near[x:positive] : Z :=
+  Cases x of 
+    xH => `0`
+  | (xO xH) => `1`
+  | (xI xH) => `2`
+  | (xO y)  => (Zs (log_near y))
+  | (xI y)  => (Zs (log_near y))
+  end.    
+
+Theorem log_near_correct1 : (p:positive)` 0 <= (log_near p)`.
+Induction p; Simpl; Intros; 
+[Elim p0; Auto with zarith | Elim p0; Auto with zarith | Trivial with zarith ].
+Intros; Apply Zle_le_S.
+Generalize H0; Elim p1; Intros; Simpl;
+    [ Assumption | Assumption | Apply ZERO_le_POS ].
+Intros; Apply Zle_le_S.
+Generalize H0; Elim p1; Intros; Simpl;
+    [ Assumption | Assumption | Apply ZERO_le_POS ].
+Save.
+
+Theorem log_near_correct2: (p:positive)
+  (log_near p)=(log_inf p)
+\/(log_near p)=(log_sup p).
+Induction p.
+Intros p0 [Einf|Esup].
+Simpl. Rewrite Einf.
+Case p0; [Left | Left | Right]; Reflexivity.
+Simpl; Rewrite Esup.
+Elim (log_sup_log_inf p0).
+Generalize (log_inf_le_log_sup p0).
+Generalize (log_sup_le_Slog_inf p0).
+Case p0; Auto with zarith.
+Intros; Omega.
+Case p0; Intros; Auto with zarith.
+Intros p0 [Einf|Esup].
+Simpl.
+Repeat Rewrite Einf.
+Case p0; Intros; Auto with zarith.
+Simpl.
+Repeat Rewrite Esup.
+Case p0; Intros; Auto with zarith.
+Auto.
+Save.
+
+(*******************
+Theorem log_near_correct: (p:positive)
+  `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))`
+  /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`.
+Intro.
+Induction p.
+Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)].
+Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup.
+Rewrite Einf1.
+Repeat Rewrite two_p_S.
+Case p0; [Left | Left | Right].
+
+Split.
+Simpl.
+Rewrite E1; Case p0; Try Reflexivity.
+Compute.
+Unfold log_near; Fold log_near.
+Unfold log_inf; Fold log_inf.
+Repeat Rewrite E1.
+Split.
+***********************************)
+
+End Log_pos.
+
+Section divers.
+
+(* Number of significative digits. *)
+
+Definition N_digits :=
+  [x:Z]Cases x of 
+       	  (POS p) => (log_inf p)
+        | (NEG p) => (log_inf p)
+	|  ZERO   => `0`
+       end.
+
+Lemma ZERO_le_N_digits : (x:Z) ` 0 <= (N_digits x)`.
+Induction x; Simpl;
+[ Apply Zle_n
+| Exact log_inf_correct1
+| Exact log_inf_correct1].
+Save.
+
+Lemma log_inf_shift_nat : 
+  (n:nat)(log_inf (shift_nat n xH))=(inject_nat n).
+Induction n; Intros;
+[ Try Trivial
+| Rewrite -> inj_S; Rewrite <- H; Reflexivity].
+Save.
+
+Lemma log_sup_shift_nat : 
+  (n:nat)(log_sup (shift_nat n xH))=(inject_nat n).
+Induction n; Intros;
+[ Try Trivial
+| Rewrite -> inj_S; Rewrite <- H; Reflexivity].
+Save.
+
+(* (Is_power p) means that p is a power of two *)
+Fixpoint Is_power[p:positive] : Prop :=
+  Cases p of
+    xH => True
+  | (xO q) => (Is_power q)
+  | (xI q) => False
+  end.
+
+Lemma Is_power_correct :
+  (p:positive) (Is_power p) <-> (Ex [y:nat](p=(shift_nat y xH))).
+
+Split; 
+[ Elim p; 
+   [ Simpl; Tauto
+   | Simpl; Intros; Generalize (H H0); Intro H1; Elim H1; Intros y0 Hy0;
+     Exists (S y0); Rewrite Hy0; Reflexivity
+   | Intro; Exists O; Reflexivity]
+| Intros; Elim H; Intros; Rewrite -> H0; Elim x; Intros; Simpl; Trivial].
+Save.
+
+Lemma Is_power_or : (p:positive) (Is_power p)\/~(Is_power p).
+Induction p;
+[ Intros; Right; Simpl; Tauto
+| Intros; Elim H; 
+   [ Intros; Left; Simpl; Exact H0
+   | Intros; Right; Simpl; Exact H0]
+| Left; Simpl; Trivial].
+Save.
+
+End divers.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
new file mode 100644
index 000000000..1d9727573
--- /dev/null
+++ b/theories/ZArith/Zpower.v
@@ -0,0 +1,386 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require ZArith.
+Require Omega.
+Require Zcomplements.
+
+Section section1.
+
+(* (Zpower_nat z n) is the n-th power of x when n is an unary
+    integer (type nat) and z an signed integer (type Z) *) 
+
+Definition Zpower_nat := 
+  [z:Z][n:nat] (iter_nat n Z ([x:Z]` z * x `) `1`).
+ 
+(* Zpower_nat_is_exp says Zpower_nat is a morphism for
+   plus : nat->nat and Zmult : Z->Z *)
+
+Lemma Zpower_nat_is_exp : 
+  (n,m:nat)(z:Z)
+  `(Zpower_nat z (plus n m)) = (Zpower_nat z n)*(Zpower_nat z m)`.
+
+Intros; Elim n; 
+[ Simpl; Elim (Zpower_nat z m); Auto with zarith
+| Unfold Zpower_nat; Intros;  Simpl; Rewrite H;
+  Apply Zmult_assoc].
+Save.
+
+(* (Zpower_nat z n) is the n-th power of x when n is an binary
+   integer (type positive) and z an signed integer (type Z) *) 
+
+Definition Zpower_pos := 
+  [z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`).
+
+(* This theorem shows that powers of unary and binary integers
+   are the same thing, modulo the function convert : positive -> nat *)
+
+Theorem Zpower_pos_nat : 
+  (z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)).
+
+Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert.
+Save.
+
+(* Using the theorem Zpower_pos_nat and the lemma Zpower_nat_is_exp we
+   deduce that the function [n:positive](Zpower_pos z n) is a morphism
+   for add : positive->positive and Zmult : Z->Z *)
+
+Theorem Zpower_pos_is_exp : 
+  (n,m:positive)(z:Z) 
+  ` (Zpower_pos z (add n m)) = (Zpower_pos z n)*(Zpower_pos z m)`.
+
+Intros.
+Rewrite -> (Zpower_pos_nat z n).
+Rewrite -> (Zpower_pos_nat z m).
+Rewrite -> (Zpower_pos_nat z (add n m)).
+Rewrite -> (convert_add n m).
+Apply Zpower_nat_is_exp.
+Save.
+
+Definition Zpower :=
+  [x,y:Z]Cases y of
+    (POS p) => (Zpower_pos x p)
+  | ZERO => `1`
+  | (NEG p) => `0`
+  end.
+
+Hints Immediate Zpower_nat_is_exp : zarith.
+Hints Immediate Zpower_pos_is_exp : zarith.
+Hints Unfold  Zpower_pos : zarith.
+Hints Unfold  Zpower_nat : zarith.
+
+Lemma Zpower_exp : (x:Z)(n,m:Z)
+  `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`.
+NewDestruct n; NewDestruct m; Auto with zarith.
+Simpl; Intros; Apply Zred_factor0.
+Simpl; Auto with zarith.
+Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
+Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
+Save.
+
+End section1.
+
+Hints Immediate Zpower_nat_is_exp : zarith.
+Hints Immediate Zpower_pos_is_exp : zarith.
+Hints Unfold  Zpower_pos : zarith.
+Hints Unfold  Zpower_nat : zarith.
+
+Section Powers_of_2.
+
+(* For the powers of two, that will be widely used, a more direct
+   calculus is possible. We will also prove some properties such
+   as (x:positive) x < 2^x that are true for all integers bigger
+   than 2 but more difficult to prove and useless. *)     
+
+(* shift n m computes 2^n * m, or m shifted by n positions *)
+
+Definition shift_nat := 
+  [n:nat][z:positive](iter_nat n positive xO z). 
+Definition shift_pos :=
+  [n:positive][z:positive](iter_pos n positive xO z). 
+Definition shift :=
+  [n:Z][z:positive]
+  Cases n of
+    ZERO => z
+  | (POS p) => (iter_pos p positive xO z)
+  | (NEG p) => z
+  end.
+
+Definition two_power_nat := [n:nat] (POS (shift_nat n xH)).
+Definition two_power_pos := [x:positive] (POS (shift_pos x xH)).
+
+Lemma two_power_nat_S : 
+  (n:nat)` (two_power_nat (S n)) = 2*(two_power_nat n)`.
+Intro; Simpl; Apply refl_equal.
+Save.
+
+Lemma shift_nat_plus :
+  (n,m:nat)(x:positive)
+    (shift_nat (plus n m) x)=(shift_nat n (shift_nat m x)).
+
+Intros; Unfold shift_nat; Apply iter_nat_plus.
+Save.
+
+Theorem shift_nat_correct :
+  (n:nat)(x:positive)(POS (shift_nat n x))=`(Zpower_nat 2 n)*(POS x)`.
+
+Unfold shift_nat; Induction n; 
+[ Simpl; Trivial with zarith
+| Intros; Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`;
+[ Rewrite <- Zmult_assoc; Rewrite <- (H x); Simpl; Reflexivity
+| Auto with zarith ]
+].
+Save.
+
+Theorem two_power_nat_correct :
+  (n:nat)(two_power_nat n)=(Zpower_nat `2` n).
+
+Intro n.
+Unfold two_power_nat.
+Rewrite -> (shift_nat_correct n).
+Omega.
+Save.
+  
+(* Second we show that two_power_pos and two_power_nat are the same *)
+Lemma shift_pos_nat : (p:positive)(x:positive)
+  (shift_pos p x)=(shift_nat (convert p) x).
+
+Unfold shift_pos.
+Unfold shift_nat.
+Intros; Apply iter_convert.
+Save.
+
+Lemma two_power_pos_nat : 
+  (p:positive) (two_power_pos p)=(two_power_nat (convert p)).
+
+Intro; Unfold two_power_pos; Unfold two_power_nat.
+Apply f_equal with f:=POS.
+Apply shift_pos_nat.
+Save.
+
+(* Then we deduce that two_power_pos is also correct *)
+
+Theorem shift_pos_correct :
+  (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`.
+
+Intros.
+Rewrite -> (shift_pos_nat p x).
+Rewrite -> (Zpower_pos_nat `2` p).
+Apply shift_nat_correct.
+Save.
+
+Theorem two_power_pos_correct : 
+  (x:positive) (two_power_pos x)=(Zpower_pos `2` x).
+
+Intro.
+Rewrite -> two_power_pos_nat.
+Rewrite -> Zpower_pos_nat.
+Apply two_power_nat_correct.
+Save.
+
+(* Some consequences *)
+
+Theorem two_power_pos_is_exp :
+  (x,y:positive) (two_power_pos (add x y))
+    =(Zmult (two_power_pos x) (two_power_pos y)).
+Intros.
+Rewrite -> (two_power_pos_correct (add x y)).
+Rewrite -> (two_power_pos_correct x).
+Rewrite -> (two_power_pos_correct y).
+Apply Zpower_pos_is_exp.
+Save.
+
+(* The exponentiation z -> 2^z for z a signed integer.   *)
+(* For convenience, we assume that 2^z = 0 for all z <0 *)
+(* We could also define a inductive type Log_result with *)
+(* 3 contructors Zero | Pos positive -> | minus_infty    *)
+(* but it's more complexe and not so useful.		 *)
+ 
+Definition two_p :=
+  [x:Z]Cases x of
+         ZERO    => `1`
+       | (POS y) => (two_power_pos y)
+       | (NEG y) => `0`
+       end.
+
+Theorem two_p_is_exp :
+  (x,y:Z) ` 0 <= x` -> ` 0 <= y` -> 
+    ` (two_p (x+y)) = (two_p x)*(two_p y)`.
+Induction x; 
+[ Induction y; Simpl; Auto with zarith
+| Induction y; 
+  [ Unfold two_p;  Rewrite -> (Zmult_sym (two_power_pos p) `1`);
+    Rewrite -> (Zmult_one (two_power_pos p)); Auto with zarith
+  | Unfold Zplus; Unfold two_p;
+    Intros; Apply two_power_pos_is_exp
+  | Intros; Unfold Zle in H0; Unfold Zcompare in H0; 
+    Absurd SUPERIEUR=SUPERIEUR; Trivial with zarith
+  ]
+| Induction y; 
+  [ Simpl; Auto with zarith
+  | Intros; Unfold Zle in H; Unfold Zcompare in H;
+    Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith
+  | Intros; Unfold Zle in H; Unfold Zcompare in H;
+    Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith
+  ]
+].
+Save.
+
+Lemma two_p_gt_ZERO : (x:Z) ` 0 <= x` -> ` (two_p x) > 0`.
+Induction x; Intros;
+[ Simpl; Omega
+| Simpl; Unfold two_power_pos; Apply POS_gt_ZERO
+| Absurd ` 0 <= (NEG p)`;
+  [ Simpl; Unfold Zle; Unfold Zcompare;
+    Do 2 Unfold not; Auto with zarith
+  | Assumption ]
+].
+Save.
+
+Lemma two_p_S : (x:Z) ` 0 <= x` -> 
+ `(two_p (Zs x)) = 2 * (two_p x)`.
+Intros; Unfold Zs. 
+Rewrite (two_p_is_exp x `1` H (ZERO_le_POS xH)).
+Apply Zmult_sym.
+Save.
+
+Lemma two_p_pred : 
+  (x:Z)` 0 <= x` -> ` (two_p (Zpred x)) < (two_p x)`.
+Intros; Apply natlike_ind 
+with P:=[x:Z]` (two_p (Zpred x)) < (two_p x)`;
+[ Simpl; Unfold Zlt; Auto with zarith
+| Intros; Elim (Zle_lt_or_eq `0` x0 H0);
+  [ Intros;
+    Replace (two_p (Zpred (Zs x0)))
+    with (two_p (Zs (Zpred x0)));
+    [ Rewrite -> (two_p_S (Zpred x0));
+      [ Rewrite -> (two_p_S x0);
+      	[ Omega
+      	| Assumption]
+      | Apply Zlt_ZERO_pred_le_ZERO; Assumption]
+    | Rewrite <- (Zs_pred x0); Rewrite <- (Zpred_Sn x0); Trivial with zarith]
+  | Intro Hx0; Rewrite <- Hx0; Simpl; Unfold Zlt; Auto with zarith]
+| Assumption].
+Save. 
+
+Lemma Zlt_lt_double : (x,y:Z) ` 0 <= x < y` -> ` x < 2*y`.
+Intros; Omega. Save. 
+
+End Powers_of_2.
+
+Hints Resolve two_p_gt_ZERO : zarith.
+Hints Immediate two_p_pred two_p_S : zarith.
+
+Section power_div_with_rest.
+
+(* Division by a power of two
+  To n:Z and p:positive q,r are associated such that
+    n = 2^p.q + r and 0 <= r < 2^p *)
+
+(* Invariant : d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d' *)
+Definition Zdiv_rest_aux :=
+  [qrd:(Z*Z)*Z] 
+  let (qr,d)=qrd in let (q,r)=qr in
+  (Cases q of
+     ZERO => ` (0, r)`
+   | (POS xH) => ` (0, d + r)`
+   | (POS (xI n)) => ` ((POS n), d + r)`
+   | (POS (xO n)) => ` ((POS n), r)`
+   | (NEG xH) => ` (-1, d + r)`
+   | (NEG (xI n)) => ` ((NEG n) - 1, d + r)`
+   | (NEG (xO n)) => ` ((NEG n), r)`
+   end, ` 2*d`).
+
+Definition Zdiv_rest := 
+  [x:Z][p:positive]let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in qr.
+
+Lemma Zdiv_rest_correct1 :
+  (x:Z)(p:positive)
+  let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in d=(two_power_pos p).
+
+Intros x p; 
+Rewrite (iter_convert p ? Zdiv_rest_aux ((x,`0`),`1`));
+Rewrite (two_power_pos_nat p);
+Elim (convert p); Simpl;
+[ Trivial with zarith
+| Intro n; Rewrite (two_power_nat_S n);
+  Unfold 2 Zdiv_rest_aux;
+  Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`));
+  NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. 
+Save.
+
+Lemma Zdiv_rest_correct2 :
+  (x:Z)(p:positive)
+  let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in
+  let (q,r)=qr in
+  ` x=q*d + r` /\ ` 0 <= r < d`.
+
+Intros; Apply iter_pos_invariant with
+  f:=Zdiv_rest_aux
+  Inv:=[qrd:(Z*Z)*Z]let (qr,d)=qrd in let (q,r)=qr in
+                      ` x=q*d + r` /\ ` 0 <= r < d`;
+[ Intro x0; Elim x0; Intro y0; Elim y0;
+  Intros q r d; Unfold Zdiv_rest_aux; 
+  Elim q;
+  [ Omega
+  | NewDestruct p0; 
+    [ Rewrite POS_xI; Intro; Elim H; Intros; Split; 
+      [ Rewrite H0; Rewrite Zplus_assoc;
+      	Rewrite Zmult_plus_distr_l;
+      	Rewrite Zmult_1_n; Rewrite Zmult_assoc;
+      	Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal
+      | Omega ]
+    | Rewrite POS_xO; Intro; Elim H; Intros; Split;
+      [ Rewrite H0;
+      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p0) `2`);
+      	Apply refl_equal  
+      | Omega ]
+    | Omega ]
+  | NewDestruct p0; 
+    [ Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; 
+      [ Rewrite H0; Rewrite Zplus_assoc;
+      	Apply f_equal with f:=[z:Z]`z+r`;
+      	Do 2 (Rewrite Zmult_plus_distr_l);
+       	Rewrite Zmult_assoc; 
+      	Rewrite (Zmult_sym (NEG p0) `2`);
+      	Rewrite <- Zplus_assoc;
+	Apply f_equal with f:=[z:Z]`2 * (NEG p0) * d + z`; 
+      	Omega
+      | Omega ]
+    | Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split;
+      [ Rewrite H0;
+      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p0) `2`);
+      	Apply refl_equal  
+      | Omega ]
+    | Omega ] ]
+| Omega].
+Save.
+
+Inductive Set Zdiv_rest_proofs[x:Z; p:positive] :=
+  Zdiv_rest_proof : (q:Z)(r:Z) 
+     `x = q * (two_power_pos p) + r` 
+       -> `0 <= r`
+        -> `r < (two_power_pos p)` 
+      	 -> (Zdiv_rest_proofs x p).
+
+Lemma  Zdiv_rest_correct :
+  (x:Z)(p:positive)(Zdiv_rest_proofs x p).
+Intros x p.
+Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p).
+Elim  (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)).
+Induction a.
+Intros.
+Elim H; Intros H1 H2; Clear H.
+Rewrite -> H0 in H1; Rewrite -> H0 in H2;
+Elim H2; Intros;
+Apply Zdiv_rest_proof with q:=a0 r:=b; Assumption.
+Save.
+
+End power_div_with_rest.
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 7eb1e37c2..bdb56fb91 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -28,6 +28,14 @@ Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR.
 Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR.
 Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR.
 
+(* Sign function *)
+Definition Zsgn [z:Z] : Z :=
+  Cases z of 
+     ZERO   => ZERO
+  | (POS p) => (POS xH)
+  | (NEG p) => (NEG xH)
+  end.
+
 (*s Absolu function *)
 Definition absolu [x:Z] : nat :=
   Cases x of
@@ -50,6 +58,31 @@ NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Save.
 
+Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x).
+Proof.
+NewDestruct x; Auto with arith.
+Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
+Save.
+
+Lemma Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
+Proof.
+NewDestruct x;Auto with arith.
+Save.
+
+Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
+NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
+Save.
+
+Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x).
+Proof.
+Destruct x;Intros;Rewrite Zmult_sym;Auto with arith.
+Save.
+
+Lemma Zabs_Zsgn: (x:Z)(Zabs x)=(Zmult (Zsgn x) x).
+Proof.
+Destruct x;Intros;Auto with arith.
+Qed.
+
 (*s From nat to Z *)
 Definition inject_nat := 
   [x:nat]Cases x of