Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of Zdiv

Some details: 

 - ZAux.v is the only file left in Ints/Z. The few elements that remain in it
   are rather specific or compatibility oriented. Others parts and files have 
   been either deleted when unused or pushed into some place of ZArith. 
 - Ints/List/ is removed since it was not needed anymore
 - Ints/Tactic.v disappear: some of its tactic were unused, some already in 
   Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict 
   has been added to Tactics.v
 - Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ...
 - A new file Zpow_facts inherits lots of results about Zpower. Placing them 
   into Zpower would have been difficult with respect to compatibility 
   (import of ring)
 - A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder
 - Adequate adaptations to Ints/num/* (mainly renaming of lemmas) 
 
Now, concerning Zdiv, the behavior when dividing by a negative number is now 
fully proved. When this was possible, existing lemmas has been extended, 
either from strictly positive to non-zero divisor, or even to arbitrary 
divisor (especially when playing with Zmod). These extended lemmas are named
with the suffix _full, whereas the original restrictive lemmas are retained 
for compatibility. Several lemmas now have shorter proofs (based on unicity 
lemmas). Lemmas are now more or less organized by themes (division and order, 
division and usual operations, etc). Three possible choices of spec for 
divisions on negative numbers are presented: this Zdiv, the ocaml approach
and the remainder-always-positive approach. The ugly behavior of Zopp 
with the current choice of Zdiv/Zmod is now fully covered. A embryo of 
division "a la Ocaml" is given: Odiv and Omod. 




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

10 files changed, 1948 insertions, 339 deletions

diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index e43d68bfa1..ab699f4a7d 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -13,6 +13,8 @@ Require Import Arith_base.
 Require Import BinPos.
 Require Import BinInt.
 Require Import Zorder.
+Require Import Zmax.
+Require Import Znat.
 Require Import ZArith_dec.
 
 Open Local Scope Z_scope.
@@ -63,6 +65,11 @@ Lemma Zabs_pos : forall n:Z, 0 <= Zabs n.
   intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H.
 Qed.
 
+Lemma Zabs_involutive : forall x:Z, Zabs (Zabs x) = Zabs x.
+Proof.
+  intros; apply Zabs_eq; apply Zabs_pos.
+Qed.
+
 Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m.
 Proof.
   intros z1 z2; case z1; case z2; simpl in |- *; auto;
@@ -96,16 +103,6 @@ Proof.
   apply Zplus_le_compat; simpl in |- *; auto with zarith.
 Qed.
 
-(** * A characterization of the sign function: *)
-
-Lemma Zsgn_spec : forall x:Z, 
-  0 < x /\ Zsgn x = 1 \/ 
-  0 = x /\ Zsgn x = 0 \/ 
-  0 > x /\ Zsgn x = -1.
-Proof. 
- intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition.
-Qed.
-
 (** * Absolute value and multiplication *)
 
 Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n.
@@ -123,25 +120,90 @@ Proof.
   intros z1 z2; case z1; case z2; simpl in |- *; auto.
 Qed.
 
-(** * Absolute value in nat is compatible with order *)
+Theorem Zabs_square : forall a, Zabs a * Zabs a = a * a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+(** * Results about absolute value in nat. *)
+
+Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
+Proof.
+  destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
+Qed.
+
+Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
+Proof.
+  destruct n; simpl; auto.
+  apply nat_of_P_o_P_of_succ_nat_eq_succ.
+Qed.
+
+Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat.
+Proof.
+  intros; apply inj_eq_rev.
+  rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult.
+Qed. 
+
+Lemma Zabs_nat_Zsucc:
+ forall p, 0 <= p ->  Zabs_nat (Zsucc p) = S (Zabs_nat p).
+Proof.
+  intros; apply inj_eq_rev.
+  rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
+Qed.
+
+Lemma Zabs_nat_Zplus: 
+ forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat.
+Proof.
+  intros; apply inj_eq_rev.
+  rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
+  apply Zplus_le_0_compat; auto.
+Qed.  
+
+Lemma Zabs_nat_Zminus:
+ forall x y, 0 <= x <= y ->  Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
+Proof.
+  intros x y (H,H').
+  assert (0 <= y) by (apply Zle_trans with x; auto).
+  assert (0 <= y-x) by (apply Zle_minus_le_0; auto).
+  apply inj_eq_rev.
+  rewrite inj_minus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
+  rewrite Zmax_right; auto.
+Qed.
+
+Lemma Zabs_nat_le :
+  forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
+Proof.
+  intros n m (H,H'); apply inj_le_rev.
+  repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
+  apply Zle_trans with n; auto.
+Qed.
 
 Lemma Zabs_nat_lt :
-  forall n m:Z, 0 <= n /\ n < m -> (Zabs_nat n < Zabs_nat m)%nat.
+  forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
 Proof.
-  intros x y. case x; simpl in |- *. case y; simpl in |- *.
+  intros n m (H,H'); apply inj_lt_rev.
+  repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
+  apply Zlt_le_weak; apply Zle_lt_trans with n; auto.
+Qed.
 
-  intro. absurd (0 < 0). compute in |- *. intro H0. discriminate H0. intuition.
-  intros. elim (ZL4 p). intros. rewrite H0. auto with arith.
-  intros. elim (ZL4 p). intros. rewrite H0. auto with arith.
-  
-  case y; simpl in |- *.
-  intros. absurd (Zpos p < 0). compute in |- *. intro H0. discriminate H0. intuition.
-  intros. change (nat_of_P p > nat_of_P p0)%nat in |- *.
-  apply nat_of_P_gt_Gt_compare_morphism.
-  elim H; auto with arith. intro. exact (ZC2 p0 p).
+(** * Some results about the sign function. *)
 
-  intros. absurd (Zpos p0 < Zneg p).
-  compute in |- *. intro H0. discriminate H0. intuition.
+Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b.
+Proof.
+  destruct a; destruct b; simpl; auto.
+Qed.
+
+Lemma Zsgn_Zopp : forall a, Zsgn (-a) = - Zsgn a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+(** A characterization of the sign function: *)
 
-  intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition.
+Lemma Zsgn_spec : forall x:Z, 
+  0 < x /\ Zsgn x = 1 \/ 
+  0 = x /\ Zsgn x = 0 \/ 
+  0 > x /\ Zsgn x = -1.
+Proof. 
+ intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition.
 Qed.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 57c0af02fa..258ae1d13d 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -70,8 +70,21 @@ Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} :
                        if r = 0 then (-q,0) else (-(q+1),b+r)
 
   In other word, when b is non-zero, q is chosen to be the greatest integer 
-  smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|.
+  smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b| (at least when 
+  r is not null). 
+*)
+
+(* Nota: At least two others conventions also exist for euclidean division.
+   They all satify the equation a=b*q+r, but differ on the choice of (q,r) 
+   on negative numbers.
+
+   * Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b).
+     Hence (-a) mod b = - (a mod b)
+           a mod (-b) = a mod b
+     And: |r| < |b| and sgn(r) = sgn(a)  (notice the a here instead of b). 
 
+   * Another solution is to always pick a non-negative remainder: 
+     a=b*q+r with 0 <= r < |b|
 *)
 
 Definition Zdiv_eucl (a b:Z) : Z * Z :=
@@ -96,7 +109,7 @@ Definition Zdiv_eucl (a b:Z) : Z * Z :=
 
 
 (** Division and modulo are projections of [Zdiv_eucl] *)
-     
+
 Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q.
 
 Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. 
@@ -108,20 +121,20 @@ Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
 
 (* Tests:
 
-Eval Compute in `(Zdiv_eucl 7 3)`. 
+Eval compute in (Zdiv_eucl 7 3). 
 
-Eval Compute in `(Zdiv_eucl (-7) 3)`.
+Eval compute in (Zdiv_eucl (-7) 3).
 
-Eval Compute in `(Zdiv_eucl 7 (-3))`.
+Eval compute in (Zdiv_eucl 7 (-3)).
 
-Eval Compute in `(Zdiv_eucl (-7) (-3))`.
+Eval compute in (Zdiv_eucl (-7) (-3)).
 
 *)
 
 
 (** * Main division theorem *) 
 
-(** First a lemma for positive *)
+(** First a lemma for two positive arguments *)
 
 Lemma Z_div_mod_POS :
   forall b:Z,
@@ -148,6 +161,7 @@ case (Zge_bool b 2); (intros; split; [ try ring | omega ]).
 omega.
 Qed.
 
+(** Then the usual situation of a positive [b] and no restriction on [a] *)
 
 Theorem Z_div_mod :
   forall a b:Z,
@@ -167,129 +181,299 @@ Proof.
   
   intros [H1 H2].
   split; trivial.
-  replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ].
+  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
   
   intros p1 [H1 H2].
   split; trivial.
-  replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ].
+  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
   generalize (Zorder.Zgt_pos_0 p1); omega.
   
   intros p1 [H1 H2].
   split; trivial.
-  replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ].
+  change (Zneg p0) with (- Zpos p0); rewrite H1; ring.
   generalize (Zorder.Zlt_neg_0 p1); omega.
   
   intros; discriminate.
 Qed.
 
-(** Existence theorems *)
+(** For stating the fully general result, let's give a short name 
+    to the condition on the remainder. *)
 
-Theorem Zdiv_eucl_exist :
-  forall b:Z,
-    b > 0 ->
-    forall a:Z, {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}.
+Definition Remainder r b :=  0 <= r < b \/ b < r <= 0.
+
+(** Another equivalent formulation: *)
+
+Definition Remainder_alt r b :=  Zabs r < Zabs b /\ Zsgn r <> - Zsgn b.
+
+(* In the last formulation, [ Zsgn r <> - Zsgn b ] is less nice than saying 
+    [ Zsgn r = Zsgn b ], but at least it works even when [r] is null. *)
+
+Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b.
 Proof.
-  intros b Hb a.
-  exists (Zdiv_eucl a b).
-  exact (Z_div_mod a b Hb).
+ intros; unfold Remainder, Remainder_alt; omega with *.
 Qed.
 
-Implicit Arguments Zdiv_eucl_exist.
+Hint Unfold Remainder.
 
-Theorem Zdiv_eucl_extended :
-  forall b:Z,
-    b <> 0 ->
-    forall a:Z,
-      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}.
+(** Now comes the fully general result about Euclidean division. *)
+
+Theorem Z_div_mod_full :
+  forall a b:Z,
+    b <> 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ Remainder r b.
+Proof.
+  destruct b as [|b|b].
+  (* b = 0 *)
+  intro H; elim H; auto.
+  (* b > 0 *)
+  intros _.
+  assert (Zpos b > 0) by auto with zarith.
+  generalize (Z_div_mod a (Zpos b) H).
+  destruct Zdiv_eucl as (q,r); intuition; simpl; auto.
+  (* b < 0 *)
+  intros _.
+  assert (Zpos b > 0) by auto with zarith.
+  generalize (Z_div_mod a (Zpos b) H).
+  unfold Remainder.
+  destruct a as [|a|a].
+  (* a = 0 *)
+  simpl; intuition.
+  (* a > 0 *)
+  unfold Zdiv_eucl; destruct Zdiv_eucl_POS as (q,r).
+  destruct r as [|r|r]; [ | | omega with *].
+  rewrite <- Zmult_opp_comm; simpl Zopp; intuition.
+  rewrite <- Zmult_opp_comm; simpl Zopp.
+  rewrite Zmult_plus_distr_r; omega with *.
+  (* a < 0 *)
+  unfold Zdiv_eucl.
+  generalize (Z_div_mod_POS (Zpos b) H a).
+  destruct Zdiv_eucl_POS as (q,r).
+  destruct r as [|r|r]; change (Zneg b) with (-Zpos b).
+  rewrite Zmult_opp_comm; omega with *.
+  rewrite <- Zmult_opp_comm, Zmult_plus_distr_r; 
+   repeat rewrite Zmult_opp_comm; omega.
+  rewrite Zmult_opp_comm; omega with *.
+Qed.
+
+(** The same results as before, stated separately in terms of Zdiv and Zmod *)
+
+Lemma Z_mod_remainder : forall a b:Z, b<>0 -> Remainder (a mod b) b.
+Proof.
+  unfold Zmod; intros a b Hb; generalize (Z_div_mod_full a b Hb); auto.
+  destruct Zdiv_eucl; tauto.
+Qed.
+
+Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= a mod b < b.
+Proof.
+  unfold Zmod; intros a b Hb; generalize (Z_div_mod a b Hb).
+  destruct Zdiv_eucl; tauto.
+Qed.
+
+Lemma Z_mod_neg : forall a b:Z, b < 0 -> b < a mod b <= 0.
+Proof.
+  unfold Zmod; intros a b Hb.
+  assert (Hb' : b<>0) by (auto with zarith).
+  generalize (Z_div_mod_full a b Hb').
+  destruct Zdiv_eucl.
+  unfold Remainder; intuition.
+Qed.
+
+Lemma Z_div_mod_eq_full : forall a b:Z, b <> 0 -> a = b*(a/b) + (a mod b).
+Proof.
+  unfold Zdiv, Zmod; intros a b Hb; generalize (Z_div_mod_full a b Hb).
+  destruct Zdiv_eucl; tauto.
+Qed.
+
+Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b*(a/b) + (a mod b).
+Proof.
+  intros; apply Z_div_mod_eq_full; auto with zarith.
+Qed.
+
+(** Existence theorem *)
+
+Theorem Zdiv_eucl_exist : forall (b:Z)(Hb: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_exist; assumption | assumption ].
-  cut (- b > 0); [ intro Hb'' | omega ].
-  elim (Zdiv_eucl_exist Hb'' a); intros qr.
-  elim qr; intros q r Hqr.
-  exists (- q, r).
-  elim Hqr; intros.
-  split.
-  rewrite <- Zmult_opp_comm; assumption.
-  rewrite Zabs_non_eq; [ assumption | omega ].
+  exists (Zdiv_eucl a b).
+  exact (Z_div_mod a b Hb).
 Qed.
 
-Implicit Arguments Zdiv_eucl_extended.
+Implicit Arguments Zdiv_eucl_exist.
+
 
 (** Uniqueness theorems *)
 
 Theorem Zdiv_mod_unique :
  forall b q1 q2 r1 r2:Z,
   0 <= r1 < Zabs b -> 0 <= r2 < Zabs b ->
-  b*q1 + r1=b*q2+r2 -> q1=q2/\r1=r2.
+  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
 Proof.
 intros b q1 q2 r1 r2 Hr1 Hr2 H.
-assert (H0:=Zeq_minus _ _ H).
-replace (b * q1 + r1 - (b * q2 + r2))
- with (b*(q1-q2) - (r2-r1)) in H0 by ring.
-assert (H1:=Zminus_eq _ _ H0).
-destruct (Z_dec q1 q2).
- elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)).
-  apply Zabs_ind;  omega.
- rewrite <- H1.
- replace (Zabs b) with (1*(Zabs b)) by ring.
- rewrite Zabs_Zmult. 
- rewrite (Zmult_comm (Zabs b)).
- apply Zmult_le_compat_r; auto with *.
- change 1 with (Zsucc 0).
- apply Zlt_le_succ.
- destruct s; apply Zabs_ind; omega.
-split; try assumption.
-rewrite e in H1.
-ring_simplify in H1.
-omega.
+destruct (Z_eq_dec q1 q2) as [Hq|Hq].
+split; trivial.
+rewrite Hq in H; omega.
+elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)).
+omega with *.
+replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega).
+replace (Zabs b) with ((Zabs b)*1) by ring.
+rewrite Zabs_Zmult. 
+apply Zmult_le_compat_l; auto with *.
+omega with *.
 Qed.
 
-(** * Auxiliary lemmas about [Zdiv] and [Zmod] *)
+Theorem Zdiv_mod_unique_2 :
+ forall b q1 q2 r1 r2:Z,
+  Remainder r1 b -> Remainder r2 b -> 
+  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.
+Proof.
+unfold Remainder.
+intros b q1 q2 r1 r2 Hr1 Hr2 H.
+destruct (Z_eq_dec q1 q2) as [Hq|Hq].
+split; trivial.
+rewrite Hq in H; omega.
+elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)).
+omega with *.
+replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega).
+replace (Zabs b) with ((Zabs b)*1) by ring.
+rewrite Zabs_Zmult.
+apply Zmult_le_compat_l; auto with *.
+omega with *.
+Qed.
 
-Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b * Zdiv a b + Zmod a b.
+Theorem Zdiv_unique_full:
+ forall a b q r, Remainder r b -> 
+   a = b*q + r -> q = a/b.
 Proof.
-  unfold Zdiv, Zmod in |- *.
-  intros a b Hb.
-  generalize (Z_div_mod a b Hb).
-  case Zdiv_eucl; tauto.
+  intros.
+  assert (b <> 0) by (unfold Remainder in *; omega with *).
+  generalize (Z_div_mod_full a b H1).
+  unfold Zdiv; destruct Zdiv_eucl as (q',r').
+  intros (H2,H3); rewrite H2 in H0.
+  destruct (Zdiv_mod_unique_2 b q q' r r'); auto.
 Qed.
 
-Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= Zmod a b < b.
+Theorem Zdiv_unique:
+ forall a b q r, 0 <= r < b -> 
+   a = b*q + r -> q = a/b.
 Proof.
-  unfold Zmod in |- *.
-  intros a b Hb.
-  generalize (Z_div_mod a b Hb).
-  case (Zdiv_eucl a b); tauto.
+  intros; eapply Zdiv_unique_full; eauto.
 Qed.
 
-Lemma Z_div_POS_ge0 :
-  forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0.
+Theorem Zmod_unique_full:
+ forall a b q r, Remainder r b ->
+  a = b*q + r ->  r = a mod b.
 Proof.
-  simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *;
-    fold Zdiv_eucl_POS in |- *; cbv zeta.
-  intro p; case (Zdiv_eucl_POS p b).
-  intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega.
-  intro p; case (Zdiv_eucl_POS p b).
-  intros; case (Zgt_bool b (2 * z0)); intros; omega.
-  case (Zge_bool b 2); simpl in |- *; omega.
+  intros.
+  assert (b <> 0) by (unfold Remainder in *; omega with *).
+  generalize (Z_div_mod_full a b H1).
+  unfold Zmod; destruct Zdiv_eucl as (q',r').
+  intros (H2,H3); rewrite H2 in H0.
+  destruct (Zdiv_mod_unique_2 b q q' r r'); auto.
 Qed.
 
-Lemma Z_div_ge0 : forall a b:Z, b > 0 -> a >= 0 -> Zdiv a b >= 0.
+Theorem Zmod_unique:
+ forall a b q r, 0 <= r < b ->
+  a = b*q + r -> r = a mod b.
 Proof.
-  intros a b Hb; unfold Zdiv, Zdiv_eucl in |- *; case a; simpl in |- *; intros.
-  case b; simpl in |- *; trivial.
-  generalize Hb; case b; try trivial.
-  auto with zarith.
-  intros p0 Hp0; generalize (Z_div_POS_ge0 (Zpos p0) p).
-  case (Zdiv_eucl_POS p (Zpos p0)); simpl in |- *; tauto.
-  intros; discriminate.
-  elim H; trivial.
+  intros; eapply Zmod_unique_full; eauto.
+Qed.
+
+(** * Basic values of divisions and modulo. *)
+
+Lemma Zmod_0_l: forall a, 0 mod a = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zmod_0_r: forall a, a mod 0 = 0.
+Proof.
+  destruct a; simpl; auto.
 Qed.
 
-Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> Zdiv a b < a.
+Lemma Zdiv_0_l: forall a, 0/a = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zdiv_0_r: forall a, a/0 = 0.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zmod_1_r: forall a, a mod 1 = 0.
+Proof.
+  intros; symmetry; apply Zmod_unique with a; auto with zarith.
+Qed.
+
+Lemma Zdiv_1_r: forall a, a/1 = a.
+Proof.
+  intros; symmetry; apply Zdiv_unique with 0; auto with zarith.
+Qed.
+
+Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r 
+ : zarith.
+
+Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0.
+Proof.
+  intros; symmetry; apply Zdiv_unique with 1; auto with zarith.
+Qed.
+
+Lemma Zmod_1_l: forall a, 1 < a ->  1 mod a = 1.
+Proof.
+  intros; symmetry; apply Zmod_unique with 0; auto with zarith.
+Qed.
+
+Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1.
+Proof.
+  intros; symmetry; apply Zdiv_unique_full with 0; auto with *; red; omega.
+Qed.
+
+Lemma Z_mod_same_full : forall a, a mod a = 0.
+Proof.
+  destruct a; intros; symmetry.
+  compute; auto.
+  apply Zmod_unique with 1; auto with *; omega with *.
+  apply Zmod_unique_full with 1; auto with *; red; omega with *.
+Qed.
+
+Lemma Z_mod_mult : forall a b, (a*b) mod b = 0.
+Proof.
+  intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; simpl; rewrite Zmod_0_r; auto.
+  symmetry; apply Zmod_unique_full with a; [ red; omega | ring ].
+Qed.
+
+Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.
+Proof.
+  intros; symmetry; apply Zdiv_unique_full with 0; auto with zarith; 
+   [ red; omega | ring].
+Qed.
+
+(** * Order results about Zmod and Zdiv *)
+
+(* Division of positive numbers is positive. *)
+
+Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b.
+Proof.
+  intros.
+  rewrite (Z_div_mod_eq a b H) in H0.
+  assert (H1:=Z_mod_lt a b H).
+  destruct (Z_lt_le_dec (a/b) 0); auto.
+  assert (b*(a/b) <= -b).
+   replace (-b) with (b*-1); [ | ring].
+   apply Zmult_le_compat_l; auto with zarith.
+  omega.
+Qed.
+
+Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0.
+Proof.
+  intros; generalize (Z_div_pos a b H); auto with zarith.
+Qed.
+
+(** As soon as the divisor is greater or equal than 2, 
+    the division is strictly decreasing. *)
+
+Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a.
 Proof.
   intros. cut (b > 0); [ intro Hb | omega ].
   generalize (Z_div_mod a b Hb).
@@ -302,9 +486,23 @@ Proof.
   auto with zarith.
 Qed.
 
-(** * Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)
+(** A division of a small number by a bigger one yields zero. *)
 
-Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a / c >= b / c.
+Theorem Zdiv_small: forall a b, 0 <= a < b -> a/b = 0.
+Proof.
+  intros a b H; apply sym_equal; apply Zdiv_unique with a; auto with zarith.
+Qed.
+
+(** Same situation, in term of modulo: *)
+
+Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a.
+Proof.
+  intros a b H; apply sym_equal; apply Zmod_unique with 0; auto with zarith.
+Qed.
+
+(** [Zge] is compatible with a positive division. *)
+
+Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c.
 Proof.
   intros a b c cPos aGeb.
   generalize (Z_div_mod_eq a c cPos).
@@ -316,13 +514,8 @@ Proof.
   intro.
   absurd (b - a >= 1).
   omega.
-  rewrite H0.
-  rewrite H2.
-  assert
-    (c * (b / c) + b mod c - (c * (a / c) + a mod c) =
-      c * (b / c - a / c) + b mod c - a mod c).
-  ring.
-  rewrite H3.
+  replace (b-a) with (c * (b/c-a/c) + b mod c - a mod c) by 
+    (symmetry; pattern a at 1; rewrite H2; pattern b at 1; rewrite H0; ring).
   assert (c * (b / c - a / c) >= c * 1).
   apply Zmult_ge_compat_l.
   omega.
@@ -332,180 +525,640 @@ Proof.
   omega.
 Qed.
 
-Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a / c <= b / c.
+(** Same, with [Zle]. *)
+
+Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c.
 Proof.
-intros a b c H H0.
-apply Zge_le.
-apply Z_div_ge; auto with *.
+  intros a b c H H0.
+  apply Zge_le.
+  apply Z_div_ge; auto with *.
 Qed.
 
-Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.
+(** With our choice of division, rounding of (a/b) is always done toward bottom: *)
+
+Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a.
 Proof.
-  intros a b c cPos.
-  generalize (Z_div_mod_eq a c cPos).
-  generalize (Z_mod_lt a c cPos).
-  generalize (Z_div_mod_eq (a + b * c) c cPos).
-  generalize (Z_mod_lt (a + b * c) c cPos).
-  intros.
+  intros a b H; generalize (Z_div_mod_eq a b H) (Z_mod_lt a b H); omega.
+Qed.
 
-  assert ((a + b * c) mod c - a mod c = c * (b + a / c - (a + b * c) / c)).
-  replace ((a + b * c) mod c) with (a + b * c - c * ((a + b * c) / c)).
-  replace (a mod c) with (a - c * (a / c)).
-  ring.
-  omega.
-  omega.
-  set (q := b + a / c - (a + b * c) / c) in *.
-  apply (Zcase_sign q); intros.
-  assert (c * q = 0).
-  rewrite H4; ring.
-  rewrite H5 in H3.
-  omega.
+Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a.
+Proof.
+  intros a b H.
+  generalize (Z_div_mod_eq_full a _ (Zlt_not_eq _ _ H)) (Z_mod_neg a _ H); omega.
+Qed.
 
-  assert (c * q >= c).
-  pattern c at 2 in |- *; replace c with (c * 1).
-  apply Zmult_ge_compat_l; omega.
-  ring.
-  omega.
+(** The previous inequalities are exact iff the modulo is zero. *)
+
+Lemma Z_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.
+Proof.
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst b; simpl in *; subst; auto.
+  generalize (Z_div_mod_eq_full a b Hb); omega.
+Qed.
+
+Lemma Z_div_exact_full_2 : forall a b:Z, b <> 0 -> a mod b = 0 -> a = b*(a/b).
+Proof.
+  intros; generalize (Z_div_mod_eq_full a b H); omega.
+Qed.
+
+(** A modulo cannot grow beyond its starting point. *)
+
+Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a.
+Proof. 
+  intros a b H1 H2; case (Zle_or_lt b a); intros H3.
+  case (Z_mod_lt a b); auto with zarith.
+  rewrite Zmod_small; auto with zarith.
+Qed.
+
+(** Some additionnal inequalities about Zdiv. *)
+
+Theorem Zdiv_le_upper_bound: 
+  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
+Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  apply Zle_trans with (2 := H3).
+  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+Qed.
+
+Theorem Zdiv_lt_upper_bound: 
+  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
+Proof.
+  intros a b q H1 H2 H3.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (2 := H3).
+  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+Qed.
+
+Theorem Zdiv_le_lower_bound: 
+  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Proof.
+  intros a b q H1 H2 H3.
+  assert (q < a / b + 1); auto with zarith.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (1 := H3).
+  pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith.
+  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (Z_mod_lt a b);
+   auto with zarith.
+Qed.
+
+(** * Relations between usual operations and Zmod and Zdiv *)
+
+Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.
+Proof.
+  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  symmetry; apply Zmod_unique_full with (a/c+b); auto with zarith.
+  red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega.
+  rewrite Zmult_plus_distr_r, Zmult_comm.
+  generalize (Z_div_mod_eq_full a c Hc); omega.
+Qed.
+
+Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b.
+Proof.
+  intro; symmetry.
+  apply Zdiv_unique_full with (a mod c); auto with zarith.
+  red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega.
+  rewrite Zmult_plus_distr_r, Zmult_comm.
+  generalize (Z_div_mod_eq_full a c H); omega.
+Qed.
+
+Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b.
+Proof.
+  intros a b c H; rewrite Zplus_comm; rewrite Z_div_plus_full;
+  try apply Zplus_comm; auto with zarith. 
+Qed.
 
-  assert (c * q <= - c).
-  replace (- c) with (c * -1).
-  apply Zmult_le_compat_l; omega.
+(** [Zopp] and [Zdiv], [Zmod].
+    Due to the choice of convention for our Euclidean division, 
+    some of the relations about [Zopp] and divisions are rather complex. *) 
+
+Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.
+Proof.
+  intros [|a|a] [|b|b]; try reflexivity; unfold Zdiv; simpl;
+  destruct (Zdiv_eucl_POS a (Zpos b)); destruct z0; try reflexivity.
+Qed.
+
+Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b).
+Proof.
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  intros; symmetry.
+  apply Zmod_unique_full with ((-a)/(-b)); auto.
+  generalize (Z_mod_remainder a b Hb); destruct 1; [right|left]; omega.
+  rewrite Zdiv_opp_opp.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb); ring.
+Qed.
+
+Lemma Z_mod_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a) mod b = 0.
+Proof.
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; rewrite Zmod_0_r; auto.
+  rewrite Z_div_exact_full_2 with a b; auto.
+  replace (- (b * (a / b))) with (0 + - (a / b) * b).
+  rewrite Z_mod_plus_full; auto.
   ring.
-  omega.
 Qed.
 
-Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b.
+Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 -> 
+ (-a) mod b = b - (a mod b).
 Proof.
-  intros a b c cPos.
-  generalize (Z_div_mod_eq a c cPos).
-  generalize (Z_mod_lt a c cPos).
-  generalize (Z_div_mod_eq (a + b * c) c cPos).
-  generalize (Z_mod_lt (a + b * c) c cPos).
   intros.
-  apply Zmult_reg_l with c. omega.
-  replace (c * ((a + b * c) / c)) with (a + b * c - (a + b * c) mod c).
-  rewrite (Z_mod_plus a b c cPos).
-  pattern a at 1 in |- *; rewrite H2.
-  ring.
-  pattern (a + b * c) at 1 in |- *; rewrite H0.
-  ring.
+  assert (b<>0) by (swap H; subst; rewrite Zmod_0_r; auto).
+  symmetry; apply Zmod_unique_full with (-1-a/b); auto.
+  generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
+  rewrite Zmult_minus_distr_l.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring.
 Qed.
 
-Lemma Zdiv_opp_opp : forall a b:Z, Zdiv (-a) (-b) = Zdiv a b.
+Lemma Z_mod_zero_opp_r : forall a b:Z, a mod b = 0 -> a mod (-b) = 0.
 Proof.
-intros [|a|a] [|b|b];
- try reflexivity;
- unfold Zdiv;
- simpl;
- destruct (Zdiv_eucl_POS a (Zpos b)); destruct z0; try reflexivity.
+  intros.
+  rewrite <- (Zopp_involutive a).
+  rewrite Zmod_opp_opp.
+  rewrite Z_mod_zero_opp_full; auto.
 Qed.
 
-Lemma Z_div_mult : forall a b:Z, b > 0 -> a * b / b = a.
-  intros; replace (a * b) with (0 + a * b); auto.
-  rewrite Z_div_plus; auto.
+Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 -> 
+ a mod (-b) = (a mod b) - b.
+Proof.
+  intros.
+  pattern a at 1; rewrite <- (Zopp_involutive a).
+  rewrite Zmod_opp_opp.
+  rewrite Z_mod_nz_opp_full; auto; omega.
 Qed.
 
-Lemma Zdiv_mult_cancel_r : forall (a b c:Z), 
- (c <> 0) -> (a*c/(b*c) = a/b).
+Lemma Z_div_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a)/b = -(a/b).
 Proof.
-assert (X: forall a b c, b > 0 -> c > 0 -> a * c / (b * c) = a / b).
+  intros; destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; do 2 rewrite Zdiv_0_r; auto.
+  symmetry; apply Zdiv_unique_full with 0; auto.
+  red; omega.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb).
+  rewrite H; ring.
+Qed.
+
+Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> 
+ (-a)/b = -(a/b)-1.
+Proof.
+  intros.
+  assert (b<>0) by (swap H; subst; rewrite Zmod_0_r; auto).
+  symmetry; apply Zdiv_unique_full with (b-a mod b); auto.
+  generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring.
+Qed.
+
+Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b).
+Proof.
+  intros.
+  pattern a at 1; rewrite <- (Zopp_involutive a).
+  rewrite Zdiv_opp_opp.
+  rewrite Z_div_zero_opp_full; auto.
+Qed.
+
+Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> 
+ a/(-b) = -(a/b)-1.
+Proof.
+  intros.
+  pattern a at 1; rewrite <- (Zopp_involutive a).
+  rewrite Zdiv_opp_opp.
+  rewrite Z_div_nz_opp_full; auto; omega.
+Qed.
+
+(** Cancellations. *)
+
+Lemma Zdiv_mult_cancel_r : forall a b c:Z, 
+ c <> 0 -> (a*c)/(b*c) = a/b.
+Proof.
+assert (X: forall a b c, b > 0 -> c > 0 -> (a*c) / (b*c) = a / b).
  intros a b c Hb Hc.
- assert (X:=Z_div_mod (a*c) (b*c)).
- assert (Y:=Z_div_mod a b Hb).
- unfold Zdiv.
- destruct (Zdiv_eucl (a*c) (b*c)).
- destruct (Zdiv_eucl a b).
- destruct Y as [Y0 Y1].
- rewrite Y0 in X.
- clear Y0.
- destruct X as [X0 X1].
-  auto with *.
- replace ((b*z1 + z2)* c) with
-  ((b*c)*z1 + z2*c) in X0 by ring.
- destruct (Zdiv_mod_unique (b*c) z1 z (z2*c) z0); try rewrite Zabs_eq; auto with *.
- split; auto with *.
- apply Zmult_lt_compat_r; auto with *.
+ symmetry.
+ apply Zdiv_unique with ((a mod b)*c); auto with zarith.
+ destruct (Z_mod_lt a b Hb); split.
+ apply Zmult_le_0_compat; auto with zarith.
+ apply Zmult_lt_compat_r; auto with zarith.
+ pattern a at 1; rewrite (Z_div_mod_eq a b Hb); ring.
 intros a b c Hc.
-destruct (Z_dec b 0) as [Hb|Hb].
- destruct Hb as [Hb|Hb];
-  destruct (not_Zeq_inf _ _ Hc).
-    rewrite <- (Zdiv_opp_opp a b).
-    replace (b*c) with ((-b)*(-c)) by ring.
-    replace (a*c) with ((-a)*(-c)) by ring.
-    apply X; auto with *.
-   rewrite <- (Zdiv_opp_opp a b).
-   rewrite <- Zdiv_opp_opp.
-   replace (-(b*c)) with ((-b)*c) by ring.
-   replace (-(a*c)) with ((-a)*c) by ring.
-   apply X; auto with *.
-  rewrite <- Zdiv_opp_opp.
-  replace (-(b*c)) with (b*(-c)) by ring.
-  replace (-(a*c)) with (a*(-c)) by ring.
-  apply X; auto with *.
- apply X; auto with *.
-rewrite Hb.
-destruct (a*c); destruct a; reflexivity.
-Qed.
-
-Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b * (a / b) <= a.
-Proof.
-  intros a b bPos.
-  generalize (Z_div_mod_eq a _ bPos); intros.
-  generalize (Z_mod_lt a _ bPos); intros.
-  pattern a at 2 in |- *; rewrite H.
-  omega.
+destruct (Z_dec b 0) as [Hb|Hb]. 
+destruct Hb as [Hb|Hb]; destruct (not_Zeq_inf _ _ Hc); auto with *.
+rewrite <- (Zdiv_opp_opp a), <- (Zmult_opp_opp b), <-(Zmult_opp_opp a); 
+ auto with *.
+rewrite <- (Zdiv_opp_opp a), <- Zdiv_opp_opp, Zopp_mult_distr_l, 
+ Zopp_mult_distr_l; auto with *.
+rewrite <- Zdiv_opp_opp, Zopp_mult_distr_r, Zopp_mult_distr_r; auto with *.
+rewrite Hb; simpl; do 2 rewrite Zdiv_0_r; auto.
 Qed.
 
-Lemma Z_mod_same : forall a:Z, a > 0 -> a mod a = 0.
+Lemma Zdiv_mult_cancel_l : forall a b c:Z, 
+ c<>0 -> (c*a)/(c*b) = a/b.
 Proof.
-  intros a aPos.
-  generalize (Z_mod_plus 0 1 a aPos).
-  replace (0 + 1 * a) with a.
   intros.
-  rewrite H.
-  compute in |- *.
-  trivial.
+  rewrite (Zmult_comm c a); rewrite (Zmult_comm c b).
+  apply Zdiv_mult_cancel_r; auto.
+Qed.
+
+Lemma Zmult_mod_distr_l: forall a b c, 
+  (c*a) mod (c*b) = c * (a mod b).
+Proof.
+  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
+  subst; simpl; rewrite Zmod_0_r; auto.
+  destruct (Z_eq_dec b 0) as [Hb|Hb].
+  subst; repeat rewrite Zmult_0_r || rewrite Zmod_0_r; auto.
+  assert (c*b <> 0).
+   contradict Hc; eapply Zmult_integral_l; eauto.
+  rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full (c*a) (c*b) H)).
+  rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full a b Hb)).
+  rewrite Zdiv_mult_cancel_l; auto with zarith.
   ring.
 Qed.
 
-Lemma Z_div_same : forall a:Z, a > 0 -> a / a = 1.
+Lemma Zmult_mod_distr_r: forall a b c, 
+  (a*c) mod (b*c) = (a mod b) * c.
+Proof.
+  intros; repeat rewrite (fun x => (Zmult_comm x c)).
+  apply Zmult_mod_distr_l; auto.
+Qed.
+
+(** Operations modulo. *)
+
+Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n.
+Proof.
+  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  pattern a at 2; rewrite (Z_div_mod_eq_full a n); auto with zarith.
+  rewrite Zplus_comm; rewrite Zmult_comm.
+  apply sym_equal; apply Z_mod_plus_full; auto with zarith.
+Qed.
+
+Theorem Zmult_mod: forall a b n,
+ (a * b) mod n = ((a mod n) * (b mod n)) mod n.
+Proof.
+  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith.
+  pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith.
+  set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n).
+  replace ((n*A' + A) * (n*B' + B))
+   with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring.
+  apply Z_mod_plus_full; auto with zarith.
+Qed.
+
+Theorem Zplus_mod: forall a b n,
+ (a + b) mod n = (a mod n + b mod n) mod n.
+Proof.
+  intros; destruct (Z_eq_dec n 0) as [Hb|Hb].
+  subst; do 2 rewrite Zmod_0_r; auto.
+  pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith.
+  pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith.
+  replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n))
+     with ((a mod n + b mod n) + (a / n + b / n) * n) by ring.
+  apply Z_mod_plus_full; auto with zarith.
+Qed.
+
+Theorem Zminus_mod: forall a b n,
+ (a - b) mod n = (a mod n - b mod n) mod n.
 Proof.
-  intros a aPos.
-  generalize (Z_div_plus 0 1 a aPos).
-  replace (0 + 1 * a) with a.
   intros.
-  rewrite H.
-  compute in |- *.
-  trivial.
+  replace (a - b) with (a + (-1) * b); auto with zarith.
+  replace (a mod n - b mod n) with (a mod n + (-1) * (b mod n)); auto with zarith.
+  rewrite Zplus_mod.
+  rewrite Zmult_mod.
+  rewrite Zplus_mod with (b:=(-1) * (b mod n)).
+  rewrite Zmult_mod.
+  rewrite Zmult_mod with (b:= b mod n).
+  repeat rewrite Zmod_mod; auto.
+Qed.
+
+Lemma Zplus_mod_idemp_l: forall a b n, (a mod n + b) mod n = (a + b) mod n.
+Proof.
+  intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto.
+Qed.
+
+Lemma Zplus_mod_idemp_r: forall a b n, (b + a mod n) mod n = (b + a) mod n.
+Proof.
+  intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto.
+Qed.
+
+Lemma Zminus_mod_idemp_l: forall a b n, (a mod n - b) mod n = (a - b) mod n.
+Proof.
+  intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto.
+Qed.
+
+Lemma Zminus_mod_idemp_r: forall a b n, (a - b mod n) mod n = (a - b) mod n.
+Proof.
+  intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto.
+Qed.
+
+Lemma Zmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.
+Proof.
+  intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto.
+Qed.
+
+Lemma Zmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.
+Proof.
+  intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto.
+Qed.
+
+Section EqualityModulo.
+ (** For a specific number n, equality modulo n is hence a nice setoid
+   equivalence, compatible with the usual operations. But for the
+   moment, Coq setoids cannot be parametric, and all this nice framework
+   will vanish at the end of this section. *)
+
+ Variable n:Z.
+
+ Definition eqm a b := (a mod n = b mod n).
+ Infix "==" := eqm (at level 70).
+
+ Lemma eqm_refl : forall a, a == a.
+ Proof. unfold eqm; auto. Qed.
+
+ Lemma eqm_sym : forall a b, a == b -> b == a.
+ Proof. unfold eqm; auto. Qed.
+
+ Lemma eqm_trans : forall a b c, a == b -> b == c -> a == c.
+ Proof. unfold eqm; eauto with *. Qed.
+
+ Add Relation Z eqm
+ reflexivity proved by eqm_refl
+ symmetry proved by eqm_sym
+ transitivity proved by eqm_trans as eqm_setoid.
+
+ Add Morphism Zplus : Zplus_eqm.
+ Proof.
+  unfold eqm; intros; rewrite Zplus_mod, H, H0, <- Zplus_mod; auto.
+ Qed.
+
+ Add Morphism Zminus : Zminus_eqm.
+ Proof.
+  unfold eqm; intros; rewrite Zminus_mod, H, H0, <- Zminus_mod; auto.
+ Qed.
+
+ Add Morphism Zmult : Zmult_eqm.
+ Proof.
+  unfold eqm; intros; rewrite Zmult_mod, H, H0, <- Zmult_mod; auto.
+ Qed.
+
+ Add Morphism Zopp : Zopp_eqm.
+ Proof.
+  intros; change (-x1 == -x2) with (0-x1 == 0-x2).
+  rewrite H; red; auto.
+ Qed.
+
+ Lemma Zmod_eqm : forall a, a mod n == a.
+ Proof. 
+  unfold eqm; intros; apply Zmod_mod.
+ Qed.
+
+ (* Zmod and Zdiv are not full morphisms with respect to eqm. 
+    For instance, take n=2. Then 3 == 1 but we don't have 
+    1 mod 3 == 1 mod 1 nor 1/3 == 1/1.
+ *)
+
+End EqualityModulo.
+
+Lemma Zdiv_Zdiv : forall a b c, b>0 -> c>0 -> (a/b)/c = a/(b*c).
+Proof.
+  intros a b c H H0.
+  pattern a at 2;rewrite (Z_div_mod_eq_full a b);auto with zarith.
+  pattern (a/b) at 2;rewrite (Z_div_mod_eq_full (a/b) c);auto with zarith.
+  replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with
+    ((a / b / c)*(b * c)  + (b * ((a / b) mod c) + a mod b)) by ring.
+  rewrite Z_div_plus_full_l; auto with zarith.
+  rewrite (Zdiv_small (b * ((a / b) mod c) + a mod b)).
   ring.
+  split.
+  apply Zplus_le_0_compat;auto with zarith.
+  apply Zmult_le_0_compat;auto with zarith.
+  destruct (Z_mod_lt (a/b) c);auto with zarith.
+  destruct (Z_mod_lt a b);auto with zarith.
+  apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)).
+  destruct (Z_mod_lt a b);auto with zarith.
+  apply Zle_lt_trans with (b * (c-1) + (b - 1)).
+  apply Zplus_le_compat;auto with zarith.
+  destruct (Z_mod_lt (a/b) c);auto with zarith.
+  replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith.
+  intro H1; 
+  assert (H2: c <> 0) by auto with zarith; 
+  rewrite (Zmult_integral_l _ _ H2 H1) in H; auto with zarith.
 Qed.
 
-Lemma Z_div_1 : forall z:Z, (z/1 = z)%Z.
+(** Unfortunately, the previous result isn't always true on negative numbers.
+    For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) *)
+
+(** A last inequality: *)
+
+Theorem Zdiv_mult_le:
+ forall a b c, 0 <= a -> 0 < b -> 0 <= c -> c*(a/b) <= (c*a)/b.
+Proof.
+  intros a b c H1 H2 H3.
+  case (Z_mod_lt a b); auto with zarith; intros Hu1 Hu2.
+  case (Z_mod_lt c b); auto with zarith; intros Hv1 Hv2.
+  apply Zmult_le_reg_r with b; auto with zarith.
+  rewrite <- Zmult_assoc.
+  replace (a / b * b) with (a - a mod b).
+  replace (c * a / b * b) with (c * a - (c * a) mod b).
+  rewrite Zmult_minus_distr_l.
+  unfold Zminus; apply Zplus_le_compat_l.
+  match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
+  apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
+  rewrite Zmult_mod; auto with zarith.
+  apply (Zmod_le ((c mod b) * (a mod b)) b); auto with zarith.
+  apply Zmult_le_compat_r; auto with zarith.
+  apply (Zmod_le c b); auto.
+  pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) b); try ring; 
+    auto with zarith.
+  pattern a at 1; rewrite (Z_div_mod_eq a b); try ring; auto with zarith.
+Qed.
+
+(** * Compatibility *)
+
+(** Weaker results kept only for compatibility *)
+
+Lemma Z_mod_same : forall a, a > 0 -> a mod a = 0.
+Proof.
+  intros; apply Z_mod_same_full.
+Qed.
+
+Lemma Z_div_same : forall a, a > 0 -> a/a = 1.
+Proof.
+  intros; apply Z_div_same_full; auto with zarith.
+Qed.
+
+Lemma Z_div_mult : forall a b:Z, b > 0 -> (a*b)/b = a.
 Proof.
-intros z.
-set (z':=z).
-unfold z' at 1.
-replace z with (0 + z*1)%Z by ring.
-rewrite (Z_div_plus 0 z 1);[reflexivity|constructor].
+  intros; apply Z_div_mult_full; auto with zarith.
 Qed.
 
-Hint Resolve Z_div_1 : zarith.
+Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.
+Proof.
+  intros; apply Z_mod_plus_full; auto with zarith.
+Qed.
 
-Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b * (a / b) -> a mod b = 0.
-  intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *.
-  case (Zdiv_eucl a b); intros q r; omega.
+Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b*(a/b) -> a mod b = 0.
+Proof.
+  intros; apply Z_div_exact_full_1; auto with zarith.
 Qed.
 
-Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b * (a / b).
-  intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *.
-  case (Zdiv_eucl a b); intros q r; omega.
+Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b*(a/b).
+Proof.
+  intros; apply Z_div_exact_full_2; auto with zarith.
 Qed.
 
-Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> - a mod b = 0.
-  intros a b Hb.
+Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0.
+Proof.
+  intros; apply Z_mod_zero_opp_full; auto with zarith.
+Qed.
+
+(** * A direct way to compute Zmod *)
+
+Fixpoint Zmod_POS (a : positive) (b : Z) {struct a} : Z  :=
+  match a with
+   | xI a' =>
+      let r := Zmod_POS a' b in
+      let r' := (2 * r + 1) in
+      if Zgt_bool b r' then r' else (r' - b)
+   | xO a' =>
+      let r := Zmod_POS a' b in
+      let r' := (2 * r) in
+      if Zgt_bool b r' then r' else (r' - b)
+   | xH => if Zge_bool b 2 then 1 else 0
+  end.
+
+Definition Zmod' a b :=
+  match a with
+   | Z0 => 0
+   | Zpos a' =>
+      match b with
+       | Z0 => 0
+       | Zpos _ => Zmod_POS a' b
+       | Zneg b' =>
+          let r := Zmod_POS a' (Zpos b') in
+          match r  with Z0 =>  0 |  _  =>   b + r end
+      end
+   | Zneg a' =>
+      match b with
+       | Z0 => 0
+       | Zpos _ =>
+          let r := Zmod_POS a' b in
+          match r with Z0 =>  0 | _  =>  b - r end
+       | Zneg b' => - (Zmod_POS a' (Zpos b'))
+      end
+  end.
+
+
+Theorem Zmod_POS_correct: forall a b, Zmod_POS a b = (snd (Zdiv_eucl_POS a b)).
+Proof.
+  intros a b; elim a; simpl; auto.
+  intros p Rec; rewrite  Rec.
+  case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto.
+  match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto.
+  intros p Rec; rewrite  Rec.
+  case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto.
+  match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto.
+  case (Zge_bool b 2); auto.
+Qed.
+
+Theorem Zmod'_correct: forall a b, Zmod' a b = Zmod a b.
+Proof.
+  intros a b; unfold Zmod; case a; simpl; auto.
+  intros p; case b; simpl; auto.
+  intros p1; refine (Zmod_POS_correct _ _); auto.
+  intros p1; rewrite Zmod_POS_correct; auto.
+  case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
+  intros p; case b; simpl; auto.
+  intros p1; rewrite Zmod_POS_correct; auto.
+  case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
+  intros p1; rewrite Zmod_POS_correct; simpl; auto.
+  case (Zdiv_eucl_POS p (Zpos p1)); auto.
+Qed.
+
+
+(** Another convention is possible for division by negative numbers:
+    * quotient is always the biggest integer smaller than or equal to a/b
+    * remainder is hence always positive or null. *)
+
+Theorem Zdiv_eucl_extended :
+  forall b:Z,
+    b <> 0 ->
+    forall a:Z,
+      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs 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_exist; assumption | assumption ].
+  cut (- b > 0); [ intro Hb'' | omega ].
+  elim (Zdiv_eucl_exist Hb'' a); intros qr.
+  elim qr; intros q r Hqr.
+  exists (- q, r).
+  elim Hqr; intros.
+  split.
+  rewrite <- Zmult_opp_comm; assumption.
+  rewrite Zabs_non_eq; [ assumption | omega ].
+Qed.
+
+Implicit Arguments Zdiv_eucl_extended.
+
+(** A third convention: Ocaml.
+     
+     Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b).
+     Hence (-a) mod b = - (a mod b)
+           a mod (-b) = a mod b
+     And: |r| < |b| and sgn(r) = sgn(a)  (notice the a here instead of b). 
+ 
+*)
+
+Definition Odiv a b := 
+  Zdiv (Zabs a) (Zabs b) * Zsgn a * Zsgn b.
+
+Definition Omod a b := 
+  Zmod (Zabs a) (Zabs b) * Zsgn a.
+
+Lemma Odiv_Omod_eq : forall a b, b<>0 -> 
+ a = b*(Odiv a b) + (Omod a b).
+Proof.
   intros.
-  rewrite Z_div_exact_2 with a b; auto.
-  replace (- (b * (a / b))) with (0 + - (a / b) * b).
-  rewrite Z_mod_plus; auto.
+  assert (Zabs b <> 0).
+   swap H.
+   destruct b; simpl in *; auto with zarith; inversion H0.
+  pattern a at 1; rewrite <- (Zabs_Zsgn a).
+  rewrite (Z_div_mod_eq_full (Zabs a) (Zabs b) H0).
+  unfold Odiv, Omod.
+  replace (b*(Zabs a/Zabs b * Zsgn a * Zsgn b)) with 
+    ((b*Zsgn b)*(Zabs a/Zabs b)*(Zsgn a)) by ring.
+  rewrite Zsgn_Zabs.
   ring.
 Qed.
+
+Lemma Odiv_opp_l : forall a b, b<>0 -> Odiv (-a) b = - (Odiv a b).
+Proof.
+  intros; unfold Odiv; rewrite Zabs_Zopp, Zsgn_Zopp; ring.
+Qed.
+
+Lemma Odiv_opp_r : forall a b, b<>0 -> Odiv a (-b) = - (Odiv a b).
+Proof.
+  intros; unfold Odiv; rewrite Zabs_Zopp, Zsgn_Zopp; ring.
+Qed.
+
+Lemma Odiv_opp_opp : forall a b, b<>0 -> Odiv (-a) (-b) = Odiv a b.
+Proof.
+  intros; unfold Odiv; do 2 rewrite Zabs_Zopp, Zsgn_Zopp; ring.
+Qed.
+
+Lemma Omod_opp_l : forall a b, b<>0 -> Omod (-a) b = - (Omod a b).
+Proof.
+  intros; unfold Omod; rewrite Zabs_Zopp, Zsgn_Zopp; ring.
+Qed.
+
+Lemma Omod_opp_r : forall a b, b<>0 -> Omod a (-b) = Omod a b.
+Proof.
+  intros; unfold Omod; rewrite Zabs_Zopp; ring.
+Qed.
+
+Lemma Omod_opp_opp : forall a b, b<>0 -> Omod (-a) (-b) = - (Omod a b).
+Proof.
+  intros; unfold Omod; do 2 rewrite Zabs_Zopp; rewrite Zsgn_Zopp; ring.
+Qed.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 0e5a03dd88..a0a75cf1eb 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -10,6 +10,8 @@
 
 Require Import BinInt.
 
+Open Scope Z_scope.
+
 (*******************************************************************)
 (** About parity: even and odd predicates on Z, division by 2 on Z *)
 
@@ -135,14 +137,14 @@ Hint Unfold Zeven Zodd: zarith.
 
 Definition Zdiv2 (z:Z) :=
   match z with
-    | Z0 => 0%Z
-    | Zpos xH => 0%Z
+    | Z0 => 0
+    | Zpos xH => 0
     | Zpos p => Zpos (Pdiv2 p)
-    | Zneg xH => 0%Z
+    | Zneg xH => 0
     | Zneg p => Zneg (Pdiv2 p)
   end.
 
-Lemma Zeven_div2 : forall n:Z, Zeven n -> n = (2 * Zdiv2 n)%Z.
+Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
 Proof.
   intro x; destruct x.
   auto with arith.
@@ -154,27 +156,27 @@ Proof.
   intros. absurd (Zeven (-1)); red in |- *; auto with arith.
 Qed.
 
-Lemma Zodd_div2 : forall n:Z, (n >= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n + 1)%Z.
+Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.
 Proof.
   intro x; destruct x.
   intros. absurd (Zodd 0); red in |- *; auto with arith.
   destruct p; auto with arith.
   intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith.
-  intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
 Qed.
 
 Lemma Zodd_div2_neg :
-  forall n:Z, (n <= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n - 1)%Z.
+  forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.
 Proof.
   intro x; destruct x.
   intros. absurd (Zodd 0); red in |- *; auto with arith.
-  intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
   destruct p; auto with arith.
   intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith.
 Qed.
 
 Lemma Z_modulo_2 :
-  forall n:Z, {y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z}.
+  forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}.
 Proof.
   intros x.
   elim (Zeven_odd_dec x); intro.
@@ -193,7 +195,7 @@ Qed.
 Lemma Zsplit2 :
   forall n:Z,
     {p : Z * Z |
-      let (x1, x2) := p in n = (x1 + x2)%Z /\ (x1 = x2 \/ x2 = (x1 + 1)%Z)}.
+      let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.
 Proof.
   intros x.
   elim (Z_modulo_2 x); intros [y Hy]; rewrite Zmult_comm in Hy;
@@ -206,3 +208,109 @@ Proof.
   right; reflexivity.
 Qed.
 
+
+Theorem Zeven_ex: forall n, Zeven n -> exists m, n = 2 * m.
+Proof.
+  intro n; exists (Zdiv2 n); apply Zeven_div2; auto.
+Qed.
+
+Theorem Zodd_ex: forall n, Zodd n -> exists m, n = 2 * m + 1.
+Proof.
+  destruct n; intros.
+  inversion H.
+  exists (Zdiv2 (Zpos p)).
+  apply Zodd_div2; simpl; auto; compute; inversion 1.
+  exists (Zdiv2 (Zneg p) - 1).
+  unfold Zminus.
+  rewrite Zmult_plus_distr_r.
+  rewrite <- Zplus_assoc.
+  assert (Zneg p <= 0) by (compute; inversion 1).
+  exact (Zodd_div2_neg _ H0 H).
+Qed.
+
+Theorem Zeven_2p: forall p, Zeven (2 * p).
+Proof.
+  destruct p; simpl; auto.
+Qed.
+
+Theorem Zodd_2p_plus_1: forall p, Zodd (2 * p + 1).
+Proof.
+  destruct p; simpl; auto.
+  destruct p; simpl; auto.
+Qed.
+
+Theorem Zeven_plus_Zodd: forall a b, 
+ Zeven a -> Zodd b -> Zodd (a + b).
+Proof.
+  intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace (2 * x + (2 * y + 1)) with (2 * (x + y) + 1); try apply Zodd_2p_plus_1; auto with zarith.
+  rewrite Zmult_plus_distr_r, Zplus_assoc; auto.
+Qed.
+
+Theorem Zeven_plus_Zeven: forall a b,
+ Zeven a -> Zeven b -> Zeven (a + b).
+Proof.
+  intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zeven_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace (2 * x + 2 * y) with (2 * (x + y)); try apply Zeven_2p; auto with zarith.
+  apply Zmult_plus_distr_r; auto.
+Qed.
+
+Theorem Zodd_plus_Zeven: forall a b, 
+ Zodd a -> Zeven b -> Zodd (a + b).
+Proof.
+  intros a b H1 H2; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto.
+Qed.
+
+Theorem Zodd_plus_Zodd: forall a b, 
+ Zodd a -> Zodd b -> Zeven (a + b).
+Proof.
+  intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace ((2 * x + 1) + (2 * y + 1)) with (2 * (x + y + 1)); try apply Zeven_2p; auto.
+  (* ring part *)
+  do 2 rewrite Zmult_plus_distr_r; auto.
+  repeat rewrite <- Zplus_assoc; f_equal.
+  rewrite (Zplus_comm 1).
+  repeat rewrite <- Zplus_assoc; auto.
+Qed.
+
+Theorem Zeven_mult_Zeven_l: forall a b, 
+ Zeven a -> Zeven (a * b).
+Proof.
+  intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  replace (2 * x * b) with (2 * (x * b)); try apply Zeven_2p; auto with zarith.
+  (* ring part *)
+  apply Zmult_assoc.
+Qed.
+
+Theorem Zeven_mult_Zeven_r: forall a b, 
+ Zeven b -> Zeven (a * b).
+Proof.
+  intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  replace (a * (2 * x)) with (2 * (x * a)); try apply Zeven_2p; auto.
+  (* ring part *)
+  rewrite (Zmult_comm x a).
+  do 2 rewrite Zmult_assoc.
+  rewrite (Zmult_comm 2 a); auto.
+Qed.
+
+Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l 
+     Zplus_assoc Zmult_1_r Zmult_1_l : Zexpand.
+
+Theorem Zodd_mult_Zodd: forall a b, 
+ Zodd a -> Zodd b -> Zodd (a * b).
+Proof.
+  intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
+  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
+  replace ((2 * x + 1) * (2 * y + 1)) with (2 * (2 * x * y + x + y) + 1); try apply Zodd_2p_plus_1; auto.
+  (* ring part *)
+  autorewrite with Zexpand; f_equal.
+  repeat rewrite <- Zplus_assoc; f_equal.
+  repeat rewrite <- Zmult_assoc; f_equal. 
+  repeat rewrite Zmult_assoc; f_equal; apply Zmult_comm.
+Qed.
+
+(* for compatibility *)
+Close Scope Z_scope.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index fbc7bfafc7..c21b4affb8 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -46,6 +46,20 @@ Proof.
  destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
 Qed.
 
+Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n.
+Proof.
+  intros n m; unfold Zmax, Zge; destruct (n ?= m); auto.
+  intro H; elim H; auto.
+Qed.
+
+Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m.
+Proof.
+  intros n m; unfold Zmax, Zle.
+  generalize (Zcompare_Eq_eq n m).
+  destruct (n ?= m); auto.
+  intros _ H; elim H; auto.
+Qed.
+
 (** * Least upper bound properties of max *)
 
 Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index d9fb4e97c2..ec37c1412f 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -256,11 +256,6 @@ Proof.
   rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
 Qed.
 
-Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
-Proof.
-destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
-Qed.
-
 (** Misc *)
 
 Theorem intro_Z :
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 262d7bac58..710c8aca08 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -293,6 +293,40 @@ Proof.
   apply Zmult_lt_compat_r; auto with zarith.
 Qed.
 
+Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m ->
+ (n | m) -> a mod n = (a mod m) mod n.
+Proof.
+  intros n m a H1 H2 H3.
+  pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith.
+  case H3; intros q Hq; pattern m at 1; rewrite Hq.
+  rewrite (Zmult_comm q).
+  rewrite Zplus_mod; auto with zarith.
+  rewrite <- Zmult_assoc; rewrite Zmult_mod; auto with zarith.
+  rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith.
+  rewrite (Zmod_small 0); auto with zarith.
+  rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith.
+Qed.
+
+Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> 
+ a mod b = c -> (b | a - c).
+Proof.
+  intros a b c H H1; apply Zmod_divide; auto with zarith.
+  rewrite Zminus_mod; auto with zarith.
+  rewrite H1; pattern c at 1; rewrite <- (Zmod_small c b); auto with zarith.
+  rewrite Zminus_diag; apply Zmod_small; auto with zarith.
+  subst; apply Z_mod_lt; auto with zarith.
+Qed.
+
+Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> 
+ (b | a - c) -> a mod b = c.
+Proof.
+  intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto.
+  replace a with ((a - c) + c); auto with zarith.
+  rewrite Zplus_mod; auto with zarith.
+  rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith.
+  rewrite Zmod_mod; try apply Zmod_small; auto with zarith.
+Qed.
+
 (** * Greatest common divisor (gcd). *)
    
 (** There is no unicity of the gcd; hence we define the predicate [gcd a b d] 
@@ -574,6 +608,7 @@ Qed.
 Lemma Zis_gcd_rel_prime :
   forall a b g:Z,
     b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).
+Proof.
   intros a b g; intros.
   assert (g <> 0).
   intro.
@@ -602,6 +637,68 @@ Lemma Zis_gcd_rel_prime :
   exists q; auto with zarith.
 Qed.
 
+Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.
+Proof.
+  intros a b H; auto with zarith.
+  red; apply Zis_gcd_sym; auto with zarith.
+Qed.
+
+Theorem rel_prime_div: forall p q r, 
+ rel_prime p q -> (r | p) -> rel_prime r q.
+Proof.
+  intros p q r H (u, H1); subst.
+  inversion_clear H as [H1 H2 H3].
+  red; apply Zis_gcd_intro; try apply Zone_divide.
+  intros x H4 H5; apply H3; auto.
+  apply Zdivide_mult_r; auto.
+Qed.
+
+Theorem rel_prime_1: forall n, rel_prime 1 n.
+Proof.
+  intros n; red; apply Zis_gcd_intro; auto.
+  exists 1; auto with zarith.
+  exists n; auto with zarith.
+Qed.
+
+Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.
+Proof.
+  intros n H H1; absurd (n = 1 \/ n = -1).
+  intros [H2 | H2]; subst; absurd_hyp H; auto with zarith.
+  case (Zis_gcd_unique  0 n n 1); auto.
+  apply Zis_gcd_intro; auto.
+  exists 0; auto with zarith.
+  exists 1; auto with zarith.
+Qed.
+
+Theorem rel_prime_mod: forall p q, 0 < q -> 
+ rel_prime p q -> rel_prime (p mod q) q.
+Proof.
+  intros p q H H0.
+  assert (H1: Bezout p q 1).
+  apply rel_prime_bezout; auto.
+  inversion_clear H1 as [q1 r1 H2].
+  apply bezout_rel_prime.
+  apply Bezout_intro with q1  (r1 + q1 * (p / q)).
+  rewrite <- H2.
+  pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith.
+Qed.
+
+Theorem rel_prime_mod_rev: forall p q, 0 < q -> 
+ rel_prime (p mod q) q -> rel_prime p q.
+Proof.
+  intros p q H H0.
+  rewrite (Z_div_mod_eq p q); auto with zarith; red.
+  apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto with zarith.
+Qed.
+
+Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.
+Proof.
+  intros a b H H1 H2.
+  case (not_rel_prime_0 _ H).
+  rewrite <- H2.
+  apply rel_prime_mod; auto with zarith.
+Qed.
+
 (** * Primality *)
 
 Inductive prime (p:Z) : Prop :=
@@ -654,6 +751,20 @@ Qed.
 
 Hint Resolve prime_rel_prime: zarith.
 
+(** As a consequence, a prime number is relatively prime with smaller numbers *)
+
+Theorem rel_prime_le_prime:
+ forall a p, prime p -> 1 <=  a < p -> rel_prime a p.
+Proof.
+  intros a p Hp [H1 H2].
+  apply rel_prime_sym; apply prime_rel_prime; auto.
+  intros [q Hq]; subst a.
+  case (Zle_or_lt q 0); intros Hl.
+  absurd (q * p <= 0 * p); auto with zarith.
+  absurd (1 * p <= q * p); auto with zarith.
+Qed.
+
+
 (** If a prime [p] divides [ab] then it divides either [a] or [b] *)
 
 Lemma prime_mult :
@@ -664,6 +775,108 @@ Proof.
   right; apply Gauss with a; auto with zarith.
 Qed.
 
+Lemma not_prime_0: ~ prime 0.
+Proof.
+  intros H1; case (prime_divisors _ H1 2); auto with zarith.
+Qed.
+
+Lemma not_prime_1: ~ prime 1.
+Proof.
+  intros H1; absurd (1 < 1); auto with zarith.
+  inversion H1; auto.
+Qed.
+ 
+Lemma prime_2: prime 2.
+Proof.
+  apply prime_intro; auto with zarith.
+  intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
+   clear H1; intros H1.
+  absurd_hyp H2; auto with zarith.
+  subst n; red; auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+Qed.
+ 
+Theorem prime_3: prime 3.
+Proof.
+  apply prime_intro; auto with zarith.
+  intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
+   clear H1; intros H1.
+  case (Zle_lt_or_eq 2 n); auto with zarith; clear H1; intros H1.
+  absurd_hyp H2; auto with zarith.
+  subst n; red; auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+  intros x [q1 Hq1] [q2 Hq2].
+  exists (q2 - q1).
+  apply trans_equal with (3 - 2); auto with zarith.
+  rewrite Hq1; rewrite Hq2; ring.
+  subst n; red; auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+Qed.
+ 
+Theorem prime_ge_2: forall p, prime p ->  2 <= p.
+Proof.
+  intros p Hp; inversion Hp; auto with zarith.
+Qed.
+
+Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)).
+
+Theorem prime_alt: 
+ forall p, prime' p <-> prime p.
+Proof.
+  split; destruct 1; intros.
+  (* prime -> prime' *)
+  constructor; auto; intros.
+  red; apply Zis_gcd_intro; auto with zarith; intros.
+  case (Zle_lt_or_eq 0 (Zabs x)); auto with zarith; intros H6.
+  case (Zle_lt_or_eq 1 (Zabs x)); auto with zarith; intros H7.
+  case (Zle_lt_or_eq (Zabs x) p); auto with zarith.
+  apply Zdivide_le; auto with zarith.
+  apply Zdivide_Zabs_inv_l; auto.
+  intros H8; case (H0 (Zabs x)); auto.
+  apply Zdivide_Zabs_inv_l; auto.
+  intros H8; subst p; absurd (Zabs x <= n); auto with zarith.
+  apply Zdivide_le; auto with zarith.
+  apply Zdivide_Zabs_inv_l; auto.
+  rewrite H7; pattern (Zabs x); apply Zabs_intro; auto with zarith.
+  absurd (0%Z = p); auto with zarith.
+  assert (x=0) by (destruct x; simpl in *; now auto).
+  subst x; elim H3; intro q; rewrite Zmult_0_r; auto.
+  (* prime' -> prime *)
+  split; auto; intros.
+  intros H2.
+  case (Zis_gcd_unique n p n 1); auto with zarith.
+  apply Zis_gcd_intro; auto with zarith.
+  apply H0; auto with zarith.
+Qed.
+ 
+Theorem square_not_prime: forall a, ~ prime (a * a).
+Proof.
+  intros a Ha.
+  rewrite <- (Zabs_square a) in Ha.
+  assert (0 <= Zabs a) by auto with zarith.
+  set (b:=Zabs a) in *; clearbody b.
+  rewrite <- prime_alt in Ha; destruct Ha.
+  case (Zle_lt_or_eq 0 b); auto with zarith; intros Hza1; [ | subst; omega].
+  case (Zle_lt_or_eq 1 b); auto with zarith; intros Hza2; [ | subst; omega].
+  assert (Hza3 := Zmult_lt_compat_r 1 b b Hza1 Hza2).
+  rewrite Zmult_1_l in Hza3.
+  elim (H1 _ (conj Hza2 Hza3)).
+  exists b; auto.
+Qed.
+
+Theorem prime_div_prime: forall p q, 
+ prime p -> prime q -> (p | q) -> p = q.
+Proof.
+  intros p q H H1 H2; 
+  assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
+  assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
+  case prime_divisors with (2 := H2); auto.
+  intros H4; absurd_hyp Hp; subst; auto with zarith.
+  intros [H4| [H4 | H4]]; subst; auto.
+  absurd_hyp H; auto; apply not_prime_1.
+  absurd_hyp Hp; auto with zarith.
+Qed.
+
 
 (** We could obtain a [Zgcd] function via Euclid algorithm. But we propose 
   here a binary version of [Zgcd], faster and executable within Coq.
@@ -895,12 +1108,12 @@ Theorem Zgcd_div_swap0 : forall a b : Z,
  0 < b ->
  (a / Zgcd a b) * b = a * (b/Zgcd a b).
 Proof.
- intros a b Hg Hb.
- assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
- pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
- repeat rewrite Zmult_assoc; f_equal.
- rewrite Zmult_comm.
- rewrite <- Zdivide_Zdiv_eq; auto.
+  intros a b Hg Hb.
+  assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
+  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+  repeat rewrite Zmult_assoc; f_equal.
+  rewrite Zmult_comm.
+  rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
 Theorem Zgcd_div_swap : forall a b c : Z, 
@@ -908,16 +1121,100 @@ Theorem Zgcd_div_swap : forall a b c : Z,
  0 < b ->
  (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b).
 Proof.
- intros a b c Hg Hb.
- assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
- pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
- repeat rewrite Zmult_assoc; f_equal.
- rewrite Zdivide_Zdiv_eq_2; auto.
- repeat rewrite <- Zmult_assoc; f_equal.
- rewrite Zmult_comm.
- rewrite <- Zdivide_Zdiv_eq; auto.
+  intros a b c Hg Hb.
+  assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].
+  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+  repeat rewrite Zmult_assoc; f_equal.
+  rewrite Zdivide_Zdiv_eq_2; auto.
+  repeat rewrite <- Zmult_assoc; f_equal.
+  rewrite Zmult_comm.
+  rewrite <- Zdivide_Zdiv_eq; auto.
+Qed.
+
+Theorem Zgcd_1_rel_prime : forall a b, 
+ Zgcd a b = 1 <-> rel_prime a b.
+Proof.
+  unfold rel_prime; split; intro H.
+  rewrite <- H; apply Zgcd_is_gcd.
+  case (Zis_gcd_unique a b (Zgcd a b) 1); auto.
+  apply Zgcd_is_gcd.
+  intros H2; absurd (0 <= Zgcd a b); auto with zarith.
+  generalize (Zgcd_is_pos a b); auto with zarith.
 Qed.
 
+Definition rel_prime_dec: forall a b, 
+ { rel_prime a b }+{ ~ rel_prime a b }.
+Proof.
+  intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1.
+  left; apply -> Zgcd_1_rel_prime; auto.
+  right; swap H1; apply <- Zgcd_1_rel_prime; auto.
+Defined.
+
+Definition prime_dec_aux:
+ forall p m,
+  { forall n, 1 < n < m -> rel_prime n p } +
+  { exists n, 1 < n < m  /\ ~ rel_prime n p }.
+Proof.
+  intros p m.
+  case (Z_lt_dec 1 m); intros H1; 
+   [ | left; intros; elimtype False; omega ].
+  pattern m; apply natlike_rec; auto with zarith.
+  left; intros; elimtype False; omega.
+  intros x Hx IH; destruct IH as [F|E].
+  destruct (rel_prime_dec x p) as [Y|N].
+  left; intros n [HH1 HH2].
+  case (Zgt_succ_gt_or_eq x n); auto with zarith.
+  intros HH3; subst x; auto.
+  case (Z_lt_dec 1 x); intros HH1.
+  right; exists x; split; auto with zarith.
+  left; intros n [HHH1 HHH2]; absurd_hyp HHH1; auto with zarith.
+  right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith.
+Defined.
+
+Definition prime_dec: forall p, { prime p }+{ ~ prime p }.
+Proof.
+  intros p; case (Z_lt_dec 1 p); intros H1.
+  case (prime_dec_aux p p); intros H2.
+  left; apply prime_intro; auto.
+  intros n [Hn1 Hn2]; case Zle_lt_or_eq with ( 1 := Hn1 ); auto.
+  intros HH; subst n.
+  red; apply Zis_gcd_intro; auto with zarith.
+  right; intros H3; inversion_clear H3 as [Hp1 Hp2].
+  case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith.
+  right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto.
+Defined.
+
+Theorem not_prime_divide:
+ forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p  /\ (n | p).
+Proof.
+  intros p Hp Hp1.
+  case (prime_dec_aux p p); intros H1.
+  elim Hp1; constructor; auto.
+  intros n [Hn1 Hn2].
+  case Zle_lt_or_eq with ( 1 := Hn1 ); auto with zarith.
+  intros H2; subst n; red; apply Zis_gcd_intro; auto with zarith.
+  case H1; intros n [Hn1 Hn2].
+  generalize (Zgcd_is_pos n p); intros Hpos.
+  case (Zle_lt_or_eq 0 (Zgcd n p)); auto with zarith; intros H3.
+  case (Zle_lt_or_eq 1 (Zgcd n p)); auto with zarith; intros H4.
+  exists (Zgcd n p); split; auto.
+  split; auto.
+  apply Zle_lt_trans with n; auto with zarith.
+  generalize (Zgcd_is_gcd n p); intros tmp; inversion_clear tmp as [Hr1 Hr2 Hr3].
+  case Hr1; intros q Hq.
+  case (Zle_or_lt q 0); auto with zarith; intros Ht.
+  absurd (n <= 0 * Zgcd n p) ; auto with zarith.
+  pattern n at 1; rewrite Hq; auto with zarith.
+  apply Zle_trans with (1 * Zgcd n p); auto with zarith.
+  pattern n at 2; rewrite Hq; auto with zarith.
+  generalize (Zgcd_is_gcd n p); intros Ht; inversion Ht; auto.
+  case Hn2; red.
+  rewrite H4; apply Zgcd_is_gcd.
+  generalize (Zgcd_is_gcd n p); rewrite <- H3; intros tmp;
+  inversion_clear tmp as [Hr1 Hr2 Hr3].
+  absurd (n = 0); auto with zarith.
+  case Hr1; auto with zarith.
+Qed.
 
 (** A Generalized Gcd that also computes Bezout coefficients.
    The algorithm is the same as for Zgcd. *)
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 45369561d1..454560b858 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Import BinPos.
 Require Import BinInt.
@@ -997,5 +997,31 @@ Proof.
     rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. 
 Qed.
 
+Lemma Zmult_lt_compat:
+  forall n m p q : Z, 0 <= n < p -> 0 <= m < q -> n * m < p * q.
+Proof.
+  intros n m p q (H1, H2) (H3,H4).
+  assert (0<p) by (apply Zle_lt_trans with n; auto).
+  assert (0<q) by (apply Zle_lt_trans with m; auto).
+  case Zle_lt_or_eq with (1 := H1); intros H5; auto with zarith.
+  case Zle_lt_or_eq with (1 := H3); intros H6; auto with zarith.
+  apply Zlt_trans with (n * q).
+  apply Zmult_lt_compat_l; auto.
+  apply Zmult_lt_compat_r; auto with zarith.
+  rewrite <- H6; rewrite Zmult_0_r; apply Zmult_lt_0_compat; auto with zarith.
+  rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith.
+Qed.
+
+Lemma Zmult_lt_compat2: 
+  forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q.
+Proof.
+  intros n m p q (H1, H2) (H3, H4).
+  apply Zle_lt_trans with (p * m).
+  apply Zmult_le_compat_r; auto.
+  apply Zlt_le_weak; auto.
+  apply Zmult_lt_compat_l; auto.
+  apply Zlt_le_trans with n; auto.
+Qed.
+
 (** For compatibility *)
 Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
new file mode 100644
index 0000000000..448fa86023
--- /dev/null
+++ b/theories/ZArith/Zpow_facts.v
@@ -0,0 +1,451 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith_base.
+Require Import ZArithRing.
+Require Import Zcomplements.
+Require Export Zpower.
+Require Import Zdiv.
+Require Import Znumtheory.
+Open Scope Z_scope.
+
+Lemma Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
+Proof.
+  intros x; unfold Zpower_pos; simpl; auto with zarith.
+Qed.
+
+Lemma Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1.
+Proof.
+  induction p.
+  (* xI *)
+  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite Zpower_pos_1_r, IHp; auto.
+  (* xO *)
+  rewrite <- Pplus_diag.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite IHp; auto.
+  (* xH *)
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+Lemma Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0.
+Proof. 
+  induction p.
+  change (xI p) with (1 + (xO p))%positive.
+  rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto.
+  rewrite <- Pplus_diag.
+  rewrite Zpower_pos_is_exp, IHp; auto.
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+Lemma Zpower_pos_pos: forall x p,
+  0 < x -> 0 < Zpower_pos x p.
+Proof.
+  induction p; intros.
+  (* xI *)
+  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+  repeat rewrite Zpower_pos_is_exp.
+  rewrite Zpower_pos_1_r.
+  repeat apply Zmult_lt_0_compat; auto.
+  (* xO *)
+  rewrite <- Pplus_diag.
+  repeat rewrite Zpower_pos_is_exp.
+  repeat apply Zmult_lt_0_compat; auto.
+  (* xH *)
+  rewrite Zpower_pos_1_r; auto.
+Qed.
+
+
+Theorem Zpower_1_r: forall z, z^1 = z.
+Proof.
+  exact Zpower_pos_1_r.
+Qed.
+
+Theorem Zpower_1_l: forall z, 0 <= z -> 1^z = 1.
+Proof.
+  destruct z; simpl; auto.
+  intros; apply Zpower_pos_1_l.
+  intros; compute in H; elim H; auto.
+Qed.
+
+Theorem Zpower_0_l: forall z, z<>0 -> 0^z = 0.
+Proof.
+  destruct z; simpl; auto with zarith.
+  intros; apply Zpower_pos_0_l.
+Qed.
+
+Theorem Zpower_0_r: forall z, z^0 = 1.
+Proof.
+  simpl; auto.
+Qed.
+
+Theorem Zpower_2: forall z, z^2 = z * z.
+Proof.
+  intros; ring.
+Qed.
+
+Theorem Zpower_gt_0: forall x y,
+  0 < x -> 0 <= y -> 0 < x^y.
+Proof.
+  destruct y; simpl; auto with zarith.
+  intros; apply Zpower_pos_pos; auto.
+  intros; compute in H0; elim H0; auto.
+Qed.
+
+Theorem Zpower_Zabs: forall a b,  Zabs (a^b) = (Zabs a)^b.
+Proof.
+  intros a b; case (Zle_or_lt 0 b).
+  intros Hb; pattern b; apply natlike_ind; auto with zarith.
+  intros x Hx Hx1; unfold Zsucc.
+  (repeat rewrite Zpower_exp); auto with zarith.
+  rewrite Zabs_Zmult; rewrite Hx1.
+  f_equal; auto.
+  replace (a ^ 1) with a; auto.
+  simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
+  simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
+  case b; simpl; auto with zarith.
+  intros p Hp; discriminate.
+Qed.
+
+Theorem Zpower_Zsucc: forall p n, 0 <= n -> p^(Zsucc n) = p * p^n.
+Proof.
+  intros p n H.
+  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+  rewrite Zpower_1_r; apply Zmult_comm.
+Qed.
+
+Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p^(q*r) = (p^q)^r.
+Proof.
+  intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto.
+  intros H3; rewrite Zmult_0_r; repeat rewrite Zpower_exp_0; auto.
+  intros r1 H3 H4 H5.
+  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+  rewrite <- H4; try rewrite Zpower_1_r; try rewrite <- Zpower_exp; try f_equal; auto with zarith.
+  ring.
+  apply Zle_ge; replace 0 with (0 * r1); try apply Zmult_le_compat_r; auto.
+Qed.
+
+Theorem Zpower_le_monotone: forall a b c, 
+ 0 < a -> 0 <= b <= c -> a^b <= a^c.
+Proof.
+  intros a b c H (H1, H2).
+  rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
+  rewrite Zpower_exp; auto with zarith.
+  apply Zmult_le_compat_l; auto with zarith.
+  assert (0 < a ^ (c - b)); auto with zarith.
+  apply Zpower_gt_0; auto with zarith.
+  apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith.
+Qed.
+
+Theorem Zpower_lt_monotone: forall a b c, 
+ 1 < a -> 0 <= b < c -> a^b < a^c.
+Proof.
+  intros a b c H (H1, H2).
+  rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
+  rewrite Zpower_exp; auto with zarith.
+  apply Zmult_lt_compat_l; auto with zarith.
+  apply Zpower_gt_0; auto with zarith.
+  assert (0 < a ^ (c - b)); auto with zarith.
+  apply Zpower_gt_0; auto with zarith.
+  apply Zlt_le_trans with (a ^1); auto with zarith.
+  rewrite Zpower_1_r; auto with zarith.
+  apply Zpower_le_monotone; auto with zarith.
+Qed.
+
+Theorem Zpower_gt_1 : forall x y, 
+  1 < x -> 0 < y -> 1 < x^y.
+Proof.
+  intros x y H1 H2.
+  replace 1 with (x ^ 0) by apply Zpower_0_r.
+  apply Zpower_lt_monotone; auto with zarith.
+Qed.
+
+Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. 
+Proof.
+  intros x y; case y; auto with zarith.
+  simpl; auto with zarith.
+  intros p H1; assert (H: 0 <= Zpos p); auto with zarith.
+  generalize H; pattern (Zpos p); apply natlike_ind; auto.
+  intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith.
+  apply Zmult_le_0_compat; auto with zarith.
+  generalize H1; case x; compute; intros; auto; discriminate.
+Qed.
+
+Theorem Zpower_le_monotone2:
+   forall a b c, 0 < a -> b <= c -> a^b <= a^c.
+Proof.
+  intros a b c H H2.
+  destruct (Z_le_gt_dec 0 b).
+  apply Zpower_le_monotone; auto.
+  replace (a^b) with 0.
+  destruct (Z_le_gt_dec 0 c).
+  destruct (Zle_lt_or_eq _ _ z0).
+  apply Zlt_le_weak;apply Zpower_gt_0;trivial.
+  rewrite <- H0;simpl;auto with zarith.
+  replace (a^c) with 0. auto with zarith.
+  destruct c;trivial;unfold Zgt in z0;discriminate z0.
+  destruct b;trivial;unfold Zgt in z;discriminate z.
+Qed.
+
+Theorem Zmult_power: forall p q r,  0 <= q -> 0 <= r -> 
+  (p*q)^r = p^r * q^r.
+Proof.
+  intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto.
+  intros r1 H3 H4 H5.
+  unfold Zsucc; rewrite Zpower_exp; auto with zarith.
+  rewrite  H4; repeat rewrite Zpower_exp; auto with zarith; ring.
+Qed.
+
+Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith.
+
+Theorem Zpower_le_monotone3: forall a b c, 
+ 0 <= c -> 0 <= a <= b -> a^c <= b^c.
+Proof.
+  intros a b c H (H1, H2).
+  generalize H; pattern c; apply natlike_ind; auto.
+  intros x HH HH1 _; unfold Zsucc; repeat rewrite Zpower_exp; auto with zarith.
+  repeat rewrite Zpower_1_r.
+  apply Zle_trans with (a^x * b); auto with zarith.
+Qed.
+
+Lemma Zpower_le_monotone_inv: forall a b c, 
+  1 < a -> 0 < b -> a^b <= a^c -> b <= c.
+Proof.
+  intros a b c H H0 H1.
+  destruct (Z_le_gt_dec b c);trivial.
+  assert (2 <= a^b).
+   apply Zle_trans with (2^b).
+   pattern 2 at 1;replace 2 with (2^1);trivial.
+   apply Zpower_le_monotone;auto with zarith.
+   apply Zpower_le_monotone3;auto with zarith.
+  assert (c > 0).
+  destruct (Z_le_gt_dec 0 c);trivial. 
+  destruct (Zle_lt_or_eq _ _ z0);auto with zarith.
+  rewrite <- H3 in H1;simpl in H1; elimtype False;omega.
+  destruct c;try discriminate z0. simpl in H1. elimtype False;omega.
+  assert (H4 := Zpower_lt_monotone a c b H). elimtype False;omega.
+Qed.
+
+Theorem Zpower_nat_Zpower: forall p q, 0 <= q -> 
+ p^q = Zpower_nat p (Zabs_nat q).
+Proof.
+  intros p1 q1; case q1; simpl.
+  intros _; exact (refl_equal _).
+  intros p2 _; apply Zpower_pos_nat.
+  intros p2 H1; case H1; auto.
+Qed.
+
+Theorem Zpower2_lt_lin: forall n, 0 <= n -> n < 2^n.
+Proof.
+  intros n; apply (natlike_ind (fun n => n < 2 ^n)); clear n.
+  simpl; auto with zarith.
+  intros n H1 H2; unfold Zsucc.
+  case (Zle_lt_or_eq _ _ H1); clear H1; intros H1.
+  apply Zle_lt_trans with (n + n); auto with zarith.
+  rewrite Zpower_exp; auto with zarith.
+  rewrite Zpower_1_r.
+  assert (tmp: forall p, p * 2 = p + p); intros; try ring;
+  rewrite tmp; auto with zarith.
+  subst n; simpl; unfold Zpower_pos; simpl; auto with zarith.
+Qed.
+
+Theorem Zpower2_le_lin: forall n, 0 <= n -> n <= 2^n.
+Proof.
+  intros; apply Zlt_le_weak; apply Zpower2_lt_lin; auto.
+Qed.
+
+
+(** * Zpower and modulo *)
+
+Theorem Zpower_mod: forall p q n, 0 < n ->
+ (p^q) mod n = ((p mod n)^q) mod n.
+Proof.
+  intros p q n Hn; case (Zle_or_lt 0 q); intros H1.
+  generalize H1; pattern q; apply natlike_ind; auto.
+  intros q1 Hq1 Rec _; unfold Zsucc; repeat rewrite Zpower_exp; repeat rewrite Zpower_1_r; auto with zarith.
+  rewrite (fun x => (Zmult_mod x p)); try rewrite Rec; auto with zarith.
+  rewrite (fun x y => (Zmult_mod (x ^y))); try f_equal; auto with zarith.
+  f_equal; auto; apply sym_equal; apply Zmod_mod; auto with zarith.
+  generalize H1; case q; simpl; auto.
+  intros; discriminate.
+Qed.
+
+(** A direct way to compute Zpower modulo **)
+
+Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z :=
+  match m with
+   | xH => a mod n
+   | xO m' =>
+      let z := Zpow_mod_pos a m' n in
+      match z with
+       | 0 => 0
+       | _ => (z * z) mod n
+      end
+   | xI m' =>
+      let z := Zpow_mod_pos a m' n in
+      match z with
+       | 0 => 0
+       | _ => (z * z * a) mod n
+      end
+  end.
+
+Definition Zpow_mod a m n := 
+  match m with 
+   | 0 => 1 
+   | Zpos p => Zpow_mod_pos a p n 
+   | Zneg p => 0 
+  end.
+
+Theorem Zpow_mod_pos_correct: forall a m n, 0 < n -> 
+ Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
+Proof.
+  intros a m; elim m; simpl; auto.
+  intros p Rec n H1; rewrite xI_succ_xO, Pplus_one_succ_r, <-Pplus_diag; auto.
+  repeat rewrite Zpower_pos_is_exp; auto.
+  repeat rewrite Rec; auto.
+  rewrite Zpower_pos_1_r.
+  repeat rewrite (fun x => (Zmult_mod x a)); auto with zarith.
+  rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. 
+  case (Zpower_pos a p mod n); auto.
+  intros p Rec n H1; rewrite <- Pplus_diag; auto.
+  repeat rewrite Zpower_pos_is_exp; auto.
+  repeat rewrite Rec; auto.
+  rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. 
+  case (Zpower_pos a p mod n); auto.
+  unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith.
+Qed.
+
+Theorem Zpow_mod_correct: forall a m n, 1 < n -> 0 <= m ->
+ Zpow_mod a m n = (a ^ m) mod n.
+Proof.
+  intros a m n; case m; simpl.
+  intros; apply sym_equal; apply Zmod_small; auto with zarith.
+  intros; apply Zpow_mod_pos_correct; auto with zarith.
+  intros p H H1; case H1; auto.
+Qed.
+
+(* Complements about power and number theory. *)
+
+Lemma Zpower_divide: forall p q, 0 < q -> (p | p ^ q).
+Proof.
+  intros p q H; exists (p ^(q - 1)).
+  pattern p at 3; rewrite <- (Zpower_1_r p); rewrite <- Zpower_exp; try f_equal; auto with zarith.
+Qed.
+
+Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> 
+ rel_prime p q -> rel_prime p (q^i).
+Proof.
+  intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi.
+  intros H; absurd_hyp H; auto with zarith.
+  intros i Hi Rec _; rewrite Zpower_Zsucc; auto.
+  apply rel_prime_mult; auto.
+  case Zle_lt_or_eq with (1 := Hi); intros Hi1; subst; auto.
+  rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
+Qed.
+
+Theorem rel_prime_Zpower: forall i j p q, 0 <= i ->  0 <= j -> 
+ rel_prime p q -> rel_prime (p^i) (q^j).
+Proof.
+  intros i j p q Hi; generalize Hi j p q; pattern i; apply natlike_ind; auto with zarith; clear i Hi j p q.
+  intros _ j p q H H1; rewrite Zpower_0_r; apply rel_prime_1.
+  intros n Hn Rec _ j p q Hj Hpq.
+  rewrite Zpower_Zsucc; auto.
+  case Zle_lt_or_eq with (1 := Hj); intros Hj1; subst.
+  apply rel_prime_sym; apply rel_prime_mult; auto.
+  apply rel_prime_sym; apply rel_prime_Zpower_r; auto with arith.
+  apply rel_prime_sym; apply Rec; auto.
+  rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
+Qed.
+
+Theorem prime_power_prime: forall p q n, 0 <= n -> 
+ prime p -> prime q -> (p | q^n)  -> p = q.
+Proof.
+  intros p q n Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.
+  rewrite Zpower_0_r; intros.
+  assert (2<=p) by (apply prime_ge_2; auto).
+  assert (p<=1) by (apply Zdivide_le; auto with zarith).
+  omega.
+  intros n1 H H1.
+  unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
+  assert (2<=p) by (apply prime_ge_2; auto).
+  assert (2<=q) by (apply prime_ge_2; auto).
+  intros H3; case prime_mult with (2 := H3); auto.
+  intros; apply prime_div_prime; auto.
+Qed.
+
+Theorem Zdivide_power_2: forall x p n, 0 <= n -> 0 <= x -> prime p ->
+ (x | p^n) -> exists m, x = p^m.
+Proof.
+  intros x p n Hn Hx; revert p n Hn; generalize Hx.
+  pattern x; apply Z_lt_induction; auto.
+  clear x Hx; intros x IH Hx p n Hn Hp H.
+  case Zle_lt_or_eq with (1 := Hx); auto; clear Hx; intros Hx; subst.
+  case (Zle_lt_or_eq 1 x); auto with zarith; clear Hx; intros Hx; subst.
+  (* x > 1 *)
+  case (prime_dec x); intros H2.
+  exists 1; rewrite Zpower_1_r; apply prime_power_prime with n; auto.
+  case not_prime_divide with (2 := H2); auto.
+  intros p1 ((H3, H4), (q1, Hq1)); subst.
+  case (IH p1) with p n; auto with zarith.
+  apply Zdivide_trans with (2 := H); exists q1; auto with zarith.
+  intros r1 Hr1.
+  case (IH q1) with p n; auto with zarith.
+  case (Zle_lt_or_eq 0 q1).
+  apply Zmult_le_0_reg_r with p1; auto with zarith.
+  split; auto with zarith.
+  pattern q1 at 1; replace q1 with (q1 * 1); auto with zarith.
+  apply Zmult_lt_compat_l; auto with zarith.
+  intros H5; subst; absurd_hyp Hx; auto with zarith.
+  apply Zmult_le_0_reg_r with p1; auto with zarith.
+  apply Zdivide_trans with (2 := H); exists p1; auto with zarith.
+  intros r2 Hr2; exists (r2 + r1); subst.
+  apply sym_equal; apply Zpower_exp.
+  generalize Hx; case r2; simpl; auto with zarith.
+  intros; red; simpl; intros; discriminate.
+  generalize H3; case r1; simpl; auto with zarith.
+  intros; red; simpl; intros; discriminate.
+  (* x = 1 *)
+  exists 0; rewrite Zpower_0_r; auto.
+  (* x = 0 *)
+  exists n; destruct H; rewrite Zmult_0_r in H; auto.
+Qed.
+
+(** * Zsquare: a direct definition of [z^2] *)
+
+Fixpoint Psquare (p: positive): positive :=
+  match p with
+   | xH => xH
+   | xO p => xO (xO (Psquare p))
+   | xI p => xI (xO (Pplus (Psquare p) p))
+  end.
+
+Definition Zsquare p :=
+  match p with 
+   | Z0 => Z0 
+   | Zpos p => Zpos (Psquare p) 
+   | Zneg p => Zpos (Psquare p)
+  end.
+
+Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive.
+Proof.
+  induction p; simpl; auto; f_equal; rewrite IHp.  
+  apply trans_equal with (xO p + xO (p*p))%positive; auto.
+  rewrite (Pplus_comm (xO p)); auto.
+  rewrite Pmult_xI_permute_r; rewrite Pplus_assoc.
+  f_equal; auto.
+  symmetry; apply Pplus_diag.
+  symmetry; apply Pmult_xO_permute_r.
+Qed.
+
+Theorem Zsquare_correct: forall p, Zsquare p = p * p.
+Proof.
+  intro p; case p; simpl; auto; intros p1; rewrite Psquare_correct; auto.
+Qed.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index a1963a9659..f3f357de11 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -14,6 +14,8 @@ Require Import Omega.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
+Infix "^" := Zpower : Z_scope.
+
 (** * Definition of powers over [Z]*)
 
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
@@ -37,7 +39,7 @@ Qed.
 (** This theorem shows that powers of unary and binary integers
    are the same thing, modulo the function convert : [positive -> nat] *)
 
-Theorem Zpower_pos_nat :
+Lemma Zpower_pos_nat :
   forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
 Proof.
   intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
@@ -48,7 +50,7 @@ Qed.
    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 :
+Lemma Zpower_pos_is_exp :
   forall (n m:positive) (z:Z),
     Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
 Proof.
@@ -60,69 +62,19 @@ Proof.
   apply Zpower_nat_is_exp.
 Qed.
 
-Theorem Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
-Proof.
-  intros x; unfold Zpower_pos; simpl; auto with zarith.
-Qed.
-
-Theorem Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1.
-Proof.
-  induction p.
-  (* xI *)
-  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
-  repeat rewrite Zpower_pos_is_exp.
-  rewrite Zpower_pos_1_r, IHp; auto.
-  (* xO *)
-  rewrite <- Pplus_diag.
-  repeat rewrite Zpower_pos_is_exp.
-  rewrite IHp; auto.
-  (* xH *)
-  rewrite Zpower_pos_1_r; auto.
-Qed.
-
-Theorem Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0.
-Proof. 
-  induction p.
-  change (xI p) with (1 + (xO p))%positive.
-  rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto.
-  rewrite <- Pplus_diag.
-  rewrite Zpower_pos_is_exp, IHp; auto.
-  rewrite Zpower_pos_1_r; auto.
-Qed.
-
-Theorem Zpower_pos_pos: forall x p, 
-  0 < x -> 0 < Zpower_pos x p.
-Proof.
-  induction p; intros.
-  (* xI *)
-  rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
-  repeat rewrite Zpower_pos_is_exp.
-  rewrite Zpower_pos_1_r.
-  repeat apply Zmult_lt_0_compat; auto.
-  (* xO *)
-  rewrite <- Pplus_diag.
-  repeat rewrite Zpower_pos_is_exp.
-  repeat apply Zmult_lt_0_compat; auto.
-  (* xH *)
-  rewrite Zpower_pos_1_r; auto.
-Qed.
-
-Infix "^" := Zpower : Z_scope.
-
 Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
 Hint Unfold Zpower_pos Zpower_nat: zarith.
 
-Lemma Zpower_exp :
+Theorem Zpower_exp :
   forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
 Proof.
   destruct n; destruct m; auto with zarith.
-  simpl in |- *; intros; apply Zred_factor0.
-  simpl in |- *; auto with zarith.
-  intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
-  intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
+  simpl; intros; apply Zred_factor0.
+  simpl; auto with zarith.
+  intros; compute in H0; elim H0; auto.
+  intros; compute in H; elim H; auto.
 Qed.
 
-
 Section Powers_of_2.
 
   (** * Powers of 2 *)
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 4a395e6f8b..00da766d89 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -148,6 +148,7 @@ Definition Zsqrt_plain (x:Z) : Z :=
   end.
 
 (** A basic theorem about Zsqrt_plain *)
+
 Theorem Zsqrt_interval :
   forall n:Z,
     0 <= n ->
@@ -162,3 +163,53 @@ Proof.
   intros p Hle; elim Hle; auto.
 Qed.
 
+(** Positivity *)
+
+Theorem Zsqrt_plain_is_pos: forall n, 0 <= n ->  0 <= Zsqrt_plain n.
+Proof.
+  intros n m; case (Zsqrt_interval n); auto with zarith.
+  intros H1 H2; case (Zle_or_lt 0 (Zsqrt_plain n)); auto.
+  intros H3; absurd_hyp H2; auto; apply Zle_not_lt.
+  apply Zle_trans with ( 2 := H1 ).
+  replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1))
+     with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1));
+  auto with zarith.
+  ring.
+Qed.
+
+(** Direct correctness on squares. *)
+
+Theorem Zsqrt_square_id: forall a, 0 <= a ->  Zsqrt_plain (a * a) = a.
+Proof.
+  intros a H.
+  generalize (Zsqrt_plain_is_pos (a * a)); auto with zarith; intros Haa.
+  case (Zsqrt_interval (a * a)); auto with zarith.
+  intros H1 H2.
+  case (Zle_or_lt a (Zsqrt_plain (a * a))); intros H3; auto.
+  case Zle_lt_or_eq with (1:=H3); auto; clear H3; intros H3.
+  absurd_hyp H1; auto; apply Zlt_not_le; auto with zarith.
+  apply Zle_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith.
+  apply Zmult_lt_compat_r; auto with zarith.
+  absurd_hyp H2; auto; apply Zle_not_lt; auto with zarith.
+  apply Zmult_le_compat; auto with zarith.
+Qed.
+
+(** [Zsqrt_plain] is increasing *)
+
+Theorem Zsqrt_le:
+ forall p q, 0 <= p <= q  ->  Zsqrt_plain p <= Zsqrt_plain q.
+Proof.
+  intros p q [H1 H2]; case Zle_lt_or_eq with (1:=H2); clear H2; intros H2; 
+  [ | subst q; auto with zarith].
+  case (Zle_or_lt (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3.
+  assert (Hp: (0 <= Zsqrt_plain q)).
+   apply Zsqrt_plain_is_pos; auto with zarith.
+  absurd (q <= p); auto with zarith.
+  apply Zle_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)).
+  case (Zsqrt_interval q); auto with zarith.
+  apply Zle_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith.
+  apply Zmult_le_compat; auto with zarith.
+  case (Zsqrt_interval p); auto with zarith.
+Qed.
+
+