Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements

 Mostly results about Zgcd (commutativity, associativity, ...).
 Slight improvement of ZMicromega.

 Beware: some lemmas of Zdiv/ Znumtheory were asking for
 too strict or useless hypothesis. Some minor glitches may occur.

 By the way, some iff lemmas about negb in Bool.v

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

9 files changed, 117 insertions, 223 deletions

diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 212478720..70eb2331c 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -299,25 +299,7 @@ Proof.
   auto with zarith.
 Qed.
 
-Lemma narrow_interval_upper_bound : forall a b x, a > 0 -> a * x  <= b -> x <= Zdiv b a.
-Proof.
-  unfold Zdiv.
-  intros.
-  generalize (Z_div_mod b a H).
-  destruct (Zdiv_eucl b a).
-  intros.
-  destruct H1.
-  destruct H2.
-  subst.
-  assert (HH :x <= z \/ z <= x -1) by (destruct (Ztrichotomy x z) ; intuition (auto with zarith)).
-  destruct HH ;auto.
-  assert (0 < a) by auto with zarith.
-  generalize (Zmult_lt_0_le_compat_r _ _ _ H4 H1).
-  intros.
-  ring_simplify in H5.
-  rewrite Zmult_comm in H5.
-  auto with zarith.
-Qed.
+(** NB: narrow_interval_upper_bound is Zdiv.Zdiv_le_lower_bound *)
 
 Require Import QArith.
 
@@ -465,23 +447,17 @@ Proof.
   induction p ; constructor ; auto.
   exists c. ring.
 Qed.
-  
 
-Lemma Zgcd_minus : forall a b c,  0 < Zgcd a b -> (a | c - b ) -> (Zgcd a b  | c).
+Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Zgcd a b | c).
 Proof.
-  intros.
-  destruct H0.
-  exists  (q * (a / (Zgcd a b)) + (b / (Zgcd a b))).
-  rewrite Zmult_comm.
-   rewrite Zmult_plus_distr_r.
-   replace  (Zgcd a b * (q * (a / Zgcd a b))) with (q * ((Zgcd a b) * (a / Zgcd a b))) by ring.
-  rewrite <- Zdivide_Zdiv_eq ; auto.
-  rewrite <- Zdivide_Zdiv_eq ; auto.
-  auto with zarith.
-  destruct (Zgcd_is_gcd a b) ; auto.
-  destruct (Zgcd_is_gcd a b) ; auto.
+  intros a b c (q,Hq).
+  destruct (Zgcd_is_gcd a b) as [(a',Ha) (b',Hb) _].
+  set (g:=Zgcd a b) in *; clearbody g.
+  exists (q * a' + b').
+  symmetry in Hq. rewrite <- Zeq_plus_swap in Hq.
+  rewrite <- Hq, Hb, Ha. ring.
 Qed.
-  
+
 Lemma Zdivide_pol_sub : forall p a b, 
   0 < Zgcd a b -> 
   Zdivide_pol a (PsubC Zminus p b) -> 
@@ -504,44 +480,6 @@ Proof.
   apply IHp2 ; assumption.
 Qed.
 
-Lemma Zgcd_com : forall a b, Zgcd a b = Zgcd b a.
-Proof.
-  intros.
-  apply Zis_gcd_gcd.
-  apply Zgcd_is_pos.
-  destruct (Zgcd_is_gcd b a).
-  constructor ; auto.
-Qed.
-
-Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
-Proof.
-  intros.
-  apply Zis_gcd_gcd.
-  apply (Zgcd_is_pos a (Zgcd b c)).
-  constructor ; auto.
-  destruct (Zgcd_is_gcd  a b).
-  apply H1.
-  destruct (Zgcd_is_gcd  a (Zgcd b c)) ; auto.
-  destruct (Zgcd_is_gcd  a (Zgcd b c)) ; auto.
-  destruct (Zgcd_is_gcd  b c) ; auto.
-  apply Zdivide_trans with (2:= H5);auto.
-  destruct (Zgcd_is_gcd b c).
-  destruct (Zgcd_is_gcd a  (Zgcd b c)).
-  apply Zdivide_trans with (2:= H0);auto.
-  (* 3 *)
-  intros.
-  destruct (Zgcd_is_gcd a (Zgcd b c)).
-  apply H3.
-  destruct (Zgcd_is_gcd a b).
-  apply Zdivide_trans with (2:= H4) ; auto.
-  destruct (Zgcd_is_gcd b c).
-  apply H6. 
-  destruct (Zgcd_is_gcd a b).
-  apply Zdivide_trans with (2:= H8) ; auto.
-  auto.  
-Qed.
-
-
 Lemma Zdivide_pol_sub_0 : forall p a, 
   Zdivide_pol a (PsubC Zminus p 0) -> 
    Zdivide_pol a p.
@@ -837,50 +775,6 @@ Proof.
   assumption.
 Qed.  
 
-Lemma negb_true : forall x, negb x = true <-> x = false.
-Proof.
-  destruct x ; simpl; intuition.
-Qed.
-
-
-Lemma Zgcd_not_max : forall a b, 0 <=  a -> Zgcd a b <> a -> ~ (a | b).
-Proof.
-  intros.
-  intro. apply H0.
-  apply Zis_gcd_gcd; auto.
-  constructor ; auto.
-  exists 1. ring.
-Qed.
-
-Lemma  Zmod_Zopp_Zdivide : forall a b , a <> 0 -> (- b) mod a = 0 -> (a | b). 
-Proof.
-  unfold Zmod.
-  intros a b.
-  generalize (Z_div_mod_full (-b) a).
-  destruct (Zdiv_eucl (-b) a).
-  intros.
-  subst.
-  exists (-z). 
-  apply H in H0. destruct H0.
-  rewrite <- Zopp_mult_distr_l.
-  rewrite Zmult_comm. auto with zarith.
-Qed.
-
-Lemma ceiling_not_div : forall a b, a <> 0 -> ~ (a | b) -> ceiling (- b) a = Zdiv (-b) a + 1.
-Proof.
-  unfold ceiling.
-  intros.
-  assert ((-b) mod a <> 0).
-   generalize (Zmod_Zopp_Zdivide a b) ; tauto.
-  revert H1.
-  unfold Zdiv, Zmod.
-  generalize (Z_div_mod_full (-b) a).
-  destruct (Zdiv_eucl (-b) a).
-  intros.
-  destruct z0 ; congruence.
-Qed.
-
-
 Lemma  genCuttingPlaneNone : forall env f, 
   genCuttingPlane f = None -> 
   eval_nformula env f -> False.
@@ -892,25 +786,18 @@ Proof.
   case_eq (Zgt_bool g 0 && (Zgt_bool c 0 && negb (Zeq_bool (Zgcd g c) g))).
   intros. 
   flatten_bool.
-  rewrite negb_true in H5.
+  rewrite negb_true_iff in H5.
   apply Zeq_bool_neq in H5.
+  contradict H5.
   rewrite <- Zgt_is_gt_bool in H3.
   rewrite <- Zgt_is_gt_bool in H.
-  simpl in H2.
-  change (RingMicromega.eval_pol 0 Zplus Zmult (fun z => z)) with eval_pol in H2.
+  apply Zis_gcd_gcd; auto with zarith.
+  constructor; auto with zarith.
+  change (eval_pol env p = 0) in H2.
   rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith.
-  revert H2.
-  generalize (eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) ; intro x.
-  intros.
-  assert (g * x >= -c) by auto with zarith.
-  assert (g * x <= -c) by auto with zarith.
-  apply narrow_interval_lower_bound in H4 ; auto.
-  apply narrow_interval_upper_bound in H6 ; auto.
-  apply Zgcd_not_max in H5; auto with zarith.
-  rewrite ceiling_not_div in H4. 
-  auto with zarith.
-  auto with zarith.
-  auto.
+  set (x:=eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) in *; clearbody x.
+  exists (-x).
+  rewrite <- Zopp_mult_distr_l, Zmult_comm; auto with zarith.
   (**)
   discriminate.
   discriminate.
@@ -918,7 +805,6 @@ Proof.
   destruct (makeCuttingPlane p) ; discriminate.
 Qed.
 
-
   
 Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl  (eval_nformula env)  l False.
 Proof.
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 2995f0515..dcb10f3cf 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -202,6 +202,16 @@ Proof.
   destruct b; trivial.
 Qed.
 
+Lemma negb_true_iff : forall b, negb b = true <-> b = false.
+Proof.
+ destruct b; intuition.
+Qed.
+
+Lemma negb_false_iff : forall b, negb b = false <-> b = true.
+Proof.
+ destruct b; intuition.
+Qed.
+
 
 (********************************)
 (** * Properties of [orb]     *)
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index ae2f0a298..7ec360a66 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -734,7 +734,7 @@ generalize (equal_mem_2 _ _ H x).
 rewrite filter_b; auto.
 rewrite empty_mem.
 rewrite H0; simpl;intros.
-replace true with (negb false);auto;apply negb_sym;auto.
+rewrite <- negb_false_iff; auto.
 Qed.
 
 Lemma for_all_mem_3: 
@@ -762,7 +762,7 @@ exists x.
 rewrite filter_b in H1; auto.
 elim (andb_prop _ _ H1).
 split;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
+rewrite <- negb_true_iff; auto.
 Qed.
 
 (** Properties of [exists] *)
@@ -794,8 +794,8 @@ Proof.
 intros.
 rewrite for_all_exists; auto.
 rewrite for_all_mem_1;auto with bool.
-intros;generalize (H x H0);intros. 
-symmetry;apply negb_sym;simpl;auto.
+intros;generalize (H x H0);intros.
+rewrite negb_true_iff; auto.
 Qed.
 
 Lemma exists_mem_2: 
@@ -803,9 +803,9 @@ Lemma exists_mem_2:
 Proof.
 intros.
 rewrite for_all_exists in H; auto.
-replace false with (negb true);auto;apply negb_sym;symmetry.
-rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
+rewrite negb_false_iff in H.
+rewrite <- negb_true_iff.
+apply for_all_mem_2 with (2:=H); auto.
 Qed.
 
 Lemma exists_mem_3: 
@@ -813,9 +813,9 @@ Lemma exists_mem_3:
 Proof.
 intros.
 rewrite for_all_exists; auto.
-symmetry;apply negb_sym;simpl.
+rewrite negb_true_iff.
 apply for_all_mem_3 with x;auto.
-rewrite H0;auto.
+rewrite negb_false_iff; auto.
 Qed.
 
 Lemma exists_mem_4: 
@@ -823,11 +823,11 @@ Lemma exists_mem_4:
 Proof.
 intros.
 rewrite for_all_exists in H; auto.
-elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
+rewrite negb_true_iff in H.
+elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto.
 elim p;intros.
 exists x;split;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
+rewrite <-negb_false_iff; auto.
 Qed.
 
 End Bool'.
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index d890d9287..a08c6e62f 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -356,20 +356,6 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  compute in H1; discriminate.
  compute; auto.
  Qed.
- 
- Lemma Zgcd_Zabs : forall z z', Zgcd (Zabs z) z' = Zgcd z z'.
- Proof.
- destruct z; simpl; auto.
- Qed.
-
- Lemma Zgcd_sym : forall p q, Zgcd p q = Zgcd q p.
- Proof.
- intros.
- apply Zis_gcd_gcd.
- apply Zgcd_is_pos.
- apply Zis_gcd_sym.
- apply Zgcd_is_gcd.
- Qed.
 
  Lemma Zdiv_gcd_zero : forall a b, b / Zgcd a b = 0 -> b <> 0 -> 
   Zgcd a b = 0.
@@ -383,12 +369,6 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  intros; subst k; simpl in *; subst b; elim H0; auto.
  Qed.
 
- Lemma Zgcd_1 : forall z, Zgcd z 1 = 1.
- Proof.
- intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
- Qed.
- Hint Resolve Zgcd_1.
-
  Lemma Zgcd_mult_rel_prime : forall a b c, 
   Zgcd a c = 1 -> Zgcd b c = 1 -> Zgcd (a*b) c = 1.
  Proof.
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index b439462db..7373acc9a 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -546,7 +546,6 @@ Section ZModulo.
   apply Z_div_pos; auto with zarith.
   subst a; auto with zarith.
   apply Zdiv_lt_upper_bound; auto with zarith.
-  subst a; auto with zarith.
   subst a.
   replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring.
   apply Zlt_le_trans with ([|a1|]*wB+wB); auto with zarith.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 82d65dafb..67411eac8 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -140,7 +140,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
   Zcompare_spec_alt Ncompare_spec_alt
   Z.spec_add N.spec_add Z.spec_mul N.spec_mul 
-  Z.spec_gcd N.spec_gcd Zgcd_Zabs
+  Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1
   spec_Z_of_N spec_Zabs_N
  : nz.
  Ltac nzsimpl := autorewrite with nz in *.
@@ -279,7 +279,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  replace (N.to_Z q) with 0%Z in * by romega.
  rewrite Zdiv_0_l in H0; discriminate.
  (* Gt *)
- simpl; auto.
+ simpl; auto with zarith.
  Qed.
 
  (** Reduction function : producing irreducible fractions *) 
@@ -304,7 +304,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros [ z | n d ].
  unfold red.
- symmetry; apply Qred_identity; simpl; auto.
+ symmetry; apply Qred_identity; simpl; auto with zarith.
  unfold red; apply strong_spec_norm.
  Qed.
    
@@ -700,7 +700,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  unfold Reduced; intros.
  rewrite strong_spec_red, Qred_iff.
  destruct x as [zx|nx dx]; destruct y as [zy|ny dy].
- simpl in *; auto.
+ simpl in *; auto with zarith.
  simpl.
  rewrite <- Qred_iff, <- strong_spec_red, strong_spec_mul_norm_Qz_Qq; auto.
  simpl.
@@ -714,10 +714,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (Hgc' := strong_spec_irred ny dx).
  destruct irred as (n1,d1); destruct irred as (n2,d2). 
  simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
- destr_neq_bool; simpl; nzsimpl; intros.
- apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
- destr_neq_bool; simpl; nzsimpl; intros.
- auto.
+ destr_neq_bool; simpl; nzsimpl; intros; auto.
+ destr_neq_bool; simpl; nzsimpl; intros; auto.
 
  revert H H0.
  rewrite 2 strong_spec_red, 2 Qred_iff; simpl.
@@ -729,8 +727,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite N_to_Z2P in *; auto.
  rewrite Z2P_correct.
 
- apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; 
-  apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; auto.
+ apply Zgcd_mult_rel_prime; rewrite Zgcd_comm;
+  apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto.
  
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
@@ -912,7 +910,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite Zabs_eq; auto with zarith.
  rewrite N_to_Z2P in *; auto.
  rewrite Z2P_correct; auto with zarith.
- rewrite Zgcd_sym; auto.
+ rewrite Zgcd_comm; auto.
  (* 0 > n *)
  destr_neq_bool; nzsimpl; simpl; auto; intros.
  destr_zcompare; simpl; nzsimpl; auto.
@@ -928,7 +926,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite N_to_Z2P in *; auto.
  rewrite Z2P_correct; auto with zarith.
  intros.
- rewrite Zgcd_sym, Zgcd_Zabs, Zgcd_sym.
+ rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm.
  apply Zis_gcd_gcd; auto with zarith.
  apply Zis_gcd_minus.
  rewrite Zopp_involutive, <- H1; apply Zgcd_is_gcd.
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
index 03e061f29..758b22817 100644
--- a/theories/ZArith/ZOdiv.v
+++ b/theories/ZArith/ZOdiv.v
@@ -547,16 +547,14 @@ Qed.
 (** Some additionnal inequalities about Zdiv. *)
 
 Theorem ZOdiv_le_upper_bound: 
-  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
+  forall a b q, 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 (ZO_div_mod_eq a b); auto with zarith.
-  rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
+  intros.
+  rewrite <- (ZO_div_mult q b); auto with zarith.
+  apply ZO_div_monotone; auto with zarith.
 Qed.
 
-Theorem ZOdiv_lt_upper_bound: 
+Theorem ZOdiv_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.
@@ -566,16 +564,12 @@ Proof.
   rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
 Qed.
 
-Theorem ZOdiv_le_lower_bound: 
-  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Theorem ZOdiv_le_lower_bound:
+  forall a b q, 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 (ZO_div_mod_eq a b); auto with zarith.
-  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b);
-   auto with zarith.
+  intros.
+  rewrite <- (ZO_div_mult q b); auto with zarith.
+  apply ZO_div_monotone; auto with zarith.
 Qed.
 
 Theorem ZOdiv_sgn: forall a b, 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 4de7e8218..f341b193e 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -588,39 +588,32 @@ 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.
+Theorem Zdiv_lt_upper_bound:
+  forall a b q, 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).
+  intros a b q H1 H2.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (2 := H2).
   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.
+Theorem Zdiv_le_upper_bound:
+  forall a b q, 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.
+  intros.
+  rewrite <- (Z_div_mult_full q b); auto with zarith.
+  apply Z_div_le; auto with zarith.
 Qed.
 
-Theorem Zdiv_le_lower_bound: 
-  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Theorem Zdiv_le_lower_bound:
+  forall a b q, 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.
+  intros.
+  rewrite <- (Z_div_mult_full q b); auto with zarith.
+  apply Z_div_le; auto with zarith.
 Qed.
 
-
 (** A division of respect opposite monotonicity for the divisor *)
 
 Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 93ec1081b..f6d73d7eb 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -201,19 +201,17 @@ Qed.
 
 (** [Zdivide] can be expressed using [Zmod]. *)
 
-Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
+Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a).
 Proof.
-  intros a b H H0.
-  apply Zdivide_intro with (a / b).
-  pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H).
-  rewrite H0; ring.
+ intros a b NZ EQ.
+ apply Zdivide_intro with (a/b).
+ rewrite (Z_div_mod_eq_full a b NZ) at 1.
+ rewrite EQ; ring.
 Qed.
 
-Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0.
+Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0.
 Proof.
-  intros a b; simple destruct 2; intros; subst.
-  change (q * b) with (0 + q * b) in |- *.
-  rewrite Z_mod_plus; auto.
+  intros a b (c,->); apply Z_mod_mult.
 Qed.
 
 (** [Zdivide] is hence decidable *)
@@ -1131,6 +1129,42 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
+Lemma Zgcd_comm : forall a b, Zgcd a b = Zgcd b a.
+Proof.
+  intros.
+  apply Zis_gcd_gcd.
+  apply Zgcd_is_pos.
+  apply Zis_gcd_sym.
+  apply Zgcd_is_gcd.
+Qed.
+
+Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
+Proof.
+  intros.
+  apply Zis_gcd_gcd.
+  apply Zgcd_is_pos.
+  destruct (Zgcd_is_gcd a b).
+  destruct (Zgcd_is_gcd b c).
+  destruct (Zgcd_is_gcd a (Zgcd b c)).
+  constructor; eauto using Zdivide_trans.
+Qed.
+
+Lemma Zgcd_Zabs : forall a b, Zgcd (Zabs a) b = Zgcd a b.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zgcd_0 : forall a, Zgcd a 0 = Zabs a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zgcd_1 : forall a, Zgcd a 1 = 1.
+Proof.
+  intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
+Qed.
+Hint Resolve Zgcd_0 Zgcd_1 : zarith.
+
 Theorem Zgcd_1_rel_prime : forall a b, 
  Zgcd a b = 1 <-> rel_prime a b.
 Proof.