Numbers: change definition of divide (compat with Znumtheory)

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

4 files changed, 12 insertions, 9 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 673276d3e..379e68544 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -60,7 +60,7 @@ Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
 Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 
-Definition divide x y := exists z, x*z = y.
+Definition divide x y := exists z, y = z*x.
 Notation "( x | y )" := (divide x y) (at level 0).
 
 Definition Even a := exists b, a = 2*b.
@@ -847,12 +847,12 @@ Qed.
 
 Lemma divide_Zpos_Zneg_r n p : (n|Zpos p) <-> (n|Zneg p).
 Proof.
- split; intros (m,H); exists (-m); now rewrite mul_opp_r, H.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H.
 Qed.
 
 Lemma divide_Zpos_Zneg_l n p : (Zpos p|n) <-> (Zneg p|n).
 Proof.
- split; intros (m,H); exists (-m); now rewrite mul_opp_r, <- mul_opp_l.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r.
 Qed.
 
 (** ** Correctness proofs for gcd *)
@@ -876,20 +876,22 @@ Qed.
 Lemma gcd_divide_l a b : (gcd a b | a).
 Proof.
  rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
- destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto.
+ destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa.
+  now rewrite mul_comm.
 Qed.
 
 Lemma gcd_divide_r a b : (gcd a b | b).
 Proof.
  rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
- destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto.
+ destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb.
+  now rewrite mul_comm.
 Qed.
 
 Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b).
 Proof.
  assert (H : forall p q r, (r|Zpos p) -> (r|Zpos q) -> (r|Zpos (Pos.gcd p q))).
   intros p q [|r|r] H H'.
-  now destruct H.
+  destruct H; now rewrite mul_comm in *.
   apply divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos.
   apply divide_Zpos_Zneg_l, divide_Zpos, Pos.gcd_greatest;
    now apply divide_Zpos, divide_Zpos_Zneg_l.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index ff221f35e..477e2e122 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -519,7 +519,7 @@ Lemma Zmod_divides : forall a b, b<>0 ->
  (a mod b = 0 <-> exists c, a = b*c).
 Proof.
  intros. rewrite Z.mod_divide; trivial.
- split; intros (c,Hc); exists c; auto.
+ split; intros (c,Hc); exists c; subst; auto with zarith.
 Qed.
 
 (** Particular case : dividing by 2 is related with parity *)
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index b9788de8b..bbc984af1 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -39,7 +39,7 @@ Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
 
 Lemma Zdivide_equiv : forall a b, Z.divide a b <-> Zdivide a b.
 Proof.
- intros a b; split; intros (c,H); exists c; rewrite Zmult_comm; auto.
+ intros a b; split; intros (c,H); now exists c.
 Qed.
 
 Lemma Zdivide_refl : forall a:Z, (a | a).
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index b8b780831..6b6ad7423 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -462,7 +462,8 @@ Lemma Zrem_divides : forall a b,
  Zrem a b = 0 <-> exists c, a = b*c.
 Proof.
  intros. zero_or_not b. firstorder.
- rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; auto.
+ rewrite Z.rem_divide; trivial.
+ split; intros (c,Hc); exists c; subst; auto with zarith.
 Qed.
 
 (** Particular case : dividing by 2 is related with parity *)