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

9 files changed, 85 insertions, 77 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index f72c1b343..e1802dbee 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -604,11 +604,9 @@ Lemma mod_divides : forall a b, b~=0 ->
  (a mod b == 0 <-> (b|a)).
 Proof.
 intros a b Hb. split.
-intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2.
- rewrite Hab; now nzsimpl.
-intros (c,Hc).
-rewrite <- Hc, mul_comm.
-now apply mod_mul.
+intros Hab. exists (a/b). rewrite mul_comm.
+ rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl.
+intros (c,Hc). rewrite Hc. now apply mod_mul.
 Qed.
 
 End ZEuclidProp.
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
index 87a95e9d7..404fc0c43 100644
--- a/theories/Numbers/Integer/Abstract/ZGcd.v
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -21,7 +21,7 @@ Module Type ZGcdProp
 
 Lemma divide_opp_l : forall n m, (-n | m) <-> (n | m).
 Proof.
- intros n m. split; intros (p,Hp); exists (-p); rewrite <- Hp.
+ intros n m. split; intros (p,Hp); exists (-p); rewrite Hp.
   now rewrite mul_opp_l, mul_opp_r.
   now rewrite mul_opp_opp.
 Qed.
@@ -29,8 +29,8 @@ Qed.
 Lemma divide_opp_r : forall n m, (n | -m) <-> (n | m).
 Proof.
  intros n m. split; intros (p,Hp); exists (-p).
-  now rewrite mul_opp_r, Hp, opp_involutive.
-  now rewrite <- Hp, mul_opp_r.
+  now rewrite mul_opp_l, <- Hp, opp_involutive.
+  now rewrite Hp, mul_opp_l.
 Qed.
 
 Lemma divide_abs_l : forall n m, (abs n | m) <-> (n | m).
@@ -53,7 +53,7 @@ Qed.
 
 Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-1.
 Proof.
- intros n (m,Hm). now apply eq_mul_1 with m.
+ intros n (m,H). rewrite mul_comm in H. now apply eq_mul_1 with m.
 Qed.
 
 Lemma divide_antisym_abs : forall n m,
@@ -210,11 +210,11 @@ Proof.
  apply gcd_unique.
  apply mul_nonneg_nonneg; trivial using gcd_nonneg, abs_nonneg.
  destruct (gcd_divide_l n m) as (q,Hq).
- rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2.
- rewrite mul_shuffle1. apply divide_factor_l.
+ rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r.
+ rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l.
  destruct (gcd_divide_r n m) as (q,Hq).
- rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2.
- rewrite mul_shuffle1. apply divide_factor_l.
+ rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r.
+ rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l.
  intros q H H'.
  destruct (gcd_bezout n m (gcd n m) (eq_refl _)) as (a & b & EQ).
  rewrite <- EQ, <- sgn_abs, mul_add_distr_l. apply divide_add_r.
@@ -257,15 +257,15 @@ Proof.
  apply le_lteq in G; destruct G as [G|G].
  destruct (gcd_divide_l n m) as (q,Hq).
  exists (gcd n m). exists q.
- split. easy.
+ split. now rewrite mul_comm.
  split. apply gcd_divide_r.
  destruct (gcd_divide_r n m) as (r,Hr).
- rewrite <- Hr in H. rewrite <- Hq in H at 1.
- rewrite <- mul_assoc in H. apply mul_divide_cancel_l in H; [|order].
+ rewrite Hr in H. rewrite Hq in H at 1.
+ rewrite mul_shuffle0 in H. apply mul_divide_cancel_r in H; [|order].
  apply gauss with r; trivial.
- apply mul_cancel_l with (gcd n m); [order|].
- rewrite mul_1_r.
- rewrite <- gcd_mul_mono_l_nonneg, Hq, Hr; order.
+ apply mul_cancel_r with (gcd n m); [order|].
+ rewrite mul_1_l.
+ rewrite <- gcd_mul_mono_r_nonneg, <- Hq, <- Hr; order.
  symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
index 052d68ab6..06af04d16 100644
--- a/theories/Numbers/Integer/Abstract/ZLcm.v
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -86,17 +86,17 @@ Qed.
 Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)).
 Proof.
  intros a b Hb. split.
- intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2.
-  rewrite Hab; now nzsimpl.
- intros (c,Hc). rewrite <- Hc, mul_comm. now apply mod_mul.
+ intros Hab. exists (a/b). rewrite mul_comm.
+ rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl.
+ intros (c,Hc). rewrite Hc. now apply mod_mul.
 Qed.
 
 Lemma rem_divide : forall a b, b~=0 -> (a rem b == 0 <-> (b|a)).
 Proof.
  intros a b Hb. split.
- intros Hab. exists (a÷b). rewrite (quot_rem a b Hb) at 2.
-  rewrite Hab; now nzsimpl.
- intros (c,Hc). rewrite <- Hc, mul_comm. now apply rem_mul.
+ intros Hab. exists (a÷b). rewrite mul_comm.
+ rewrite (quot_rem a b Hb) at 1. rewrite Hab; now nzsimpl.
+ intros (c,Hc). rewrite Hc. now apply rem_mul.
 Qed.
 
 Lemma rem_mod_eq_0 : forall a b, b~=0 -> (a rem b == 0 <-> a mod b == 0).
@@ -248,7 +248,7 @@ Qed.
 Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a).
 Proof.
  intros a b c Ha Hb (c',Hc). exists c'.
- now rewrite mul_comm, <- divide_div_mul_exact, mul_comm, Hc.
+ now rewrite <- divide_div_mul_exact, <- Hc.
 Qed.
 
 Lemma lcm_least : forall a b c,
@@ -262,14 +262,14 @@ Proof.
  set (g:=gcd a b) in *.
  assert (Ha' := divide_div g a c NEQ Ga Ha).
  assert (Hb' := divide_div g b c NEQ Gb Hb).
- destruct Ha' as (a',Ha'). rewrite <- Ha' in Hb'.
+ destruct Ha' as (a',Ha'). rewrite Ha', mul_comm in Hb'.
  apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm].
  destruct Hb' as (b',Hb').
  exists b'.
- rewrite <- mul_assoc, Hb'.
+ rewrite mul_shuffle3, <- Hb'.
  rewrite (proj2 (div_exact c g NEQ)).
- rewrite <- Ha', mul_assoc. f_equiv.
- apply div_exact; trivial.
+ rewrite Ha', mul_shuffle3, (mul_comm a a'). f_equiv.
+ symmetry. apply div_exact; trivial.
  apply mod_divide; trivial.
  apply mod_divide; trivial. transitivity a; trivial.
 Qed.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index e3fc512e7..44dd2c593 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -409,7 +409,7 @@ Qed.
 
 (** Gcd *)
 
-Definition divide n m := exists p, n*p == m.
+Definition divide n m := exists p, m == p*n.
 Local Notation "( x | y )" := (divide x y) (at level 0).
 
 Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m].
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index 6788cd4e8..f72023d92 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -18,7 +18,7 @@ End Gcd.
 
 Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A).
  Import A B.
- Definition divide n m := exists p, n*p == m.
+ Definition divide n m := exists p, m == p*n.
  Local Notation "( n | m )" := (divide n m) (at level 0).
  Axiom gcd_divide_l : forall n m, (gcd n m | n).
  Axiom gcd_divide_r : forall n m, (gcd n m | m).
@@ -83,9 +83,17 @@ Proof.
  rewrite <- Hn, mul_0_l in H. order'.
 Qed.
 
+Lemma eq_mul_1_nonneg' : forall n m,
+ 0<=m -> n*m == 1 -> n==1 /\ m==1.
+Proof.
+ intros n m Hm H. rewrite mul_comm in H.
+ now apply and_comm, eq_mul_1_nonneg.
+Qed.
+
 Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1.
 Proof.
- intros n Hn (m,Hm). now apply (eq_mul_1_nonneg n m).
+ intros n Hn (m,Hm). symmetry in Hm.
+ now apply (eq_mul_1_nonneg' m n).
 Qed.
 
 Lemma divide_refl : forall n, (n | n).
@@ -95,8 +103,8 @@ Qed.
 
 Lemma divide_trans : forall n m p, (n | m) -> (m | p) -> (n | p).
 Proof.
- intros n m p (q,Hq) (r,Hr). exists (q*r).
- now rewrite mul_assoc, Hq.
+ intros n m p (q,Hq) (r,Hr). exists (r*q).
+ now rewrite Hr, Hq, mul_assoc.
 Qed.
 
 Instance divide_reflexive : Reflexive divide := divide_refl.
@@ -110,29 +118,29 @@ Proof.
  intros n m Hn Hm (q,Hq) (r,Hr).
  le_elim Hn.
  destruct (lt_ge_cases q 0) as [Hq'|Hq'].
- generalize (mul_pos_neg n q Hn Hq'). order.
- rewrite <- Hq, <- mul_assoc in Hr.
- apply mul_id_r in Hr; [|order].
- destruct (eq_mul_1_nonneg q r) as [H _]; trivial.
- now rewrite H, mul_1_r in Hq.
- rewrite <- Hn, mul_0_l in Hq. now rewrite <- Hn.
+ generalize (mul_neg_pos q n Hq' Hn). order.
+ rewrite Hq, mul_assoc in Hr. symmetry in Hr.
+ apply mul_id_l in Hr; [|order].
+ destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial.
+ now rewrite H, mul_1_l in Hq.
+ rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn.
 Qed.
 
 Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m).
 Proof.
- intros n m p (q,Hq). exists q. now rewrite <- mul_assoc, Hq.
+ intros n m p (q,Hq). exists q. now rewrite mul_shuffle3, Hq.
 Qed.
 
 Lemma mul_divide_mono_r : forall n m p, (n | m) -> (n * p | m * p).
 Proof.
- intros n m p (q,Hq). exists q. now rewrite mul_shuffle0, Hq.
+ intros n m p (q,Hq). exists q. now rewrite mul_assoc, Hq.
 Qed.
 
 Lemma mul_divide_cancel_l : forall n m p, p ~= 0 ->
  ((p * n | p * m) <-> (n | m)).
 Proof.
  intros n m p Hp. split.
- intros (q,Hq). exists q. now rewrite <- mul_assoc, mul_cancel_l in Hq.
+ intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq.
  apply mul_divide_mono_l.
 Qed.
 
@@ -145,12 +153,12 @@ Qed.
 Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p).
 Proof.
  intros n m p (q,Hq) (r,Hr). exists (q+r).
- now rewrite mul_add_distr_l, Hq, Hr.
+ now rewrite mul_add_distr_r, Hq, Hr.
 Qed.
 
 Lemma divide_mul_l : forall n m p, (n | m) -> (n | m * p).
 Proof.
- intros n m p (q,Hq). exists (q*p). now rewrite mul_assoc, Hq.
+ intros n m p (q,Hq). exists (q*p). now rewrite mul_shuffle0, Hq.
 Qed.
 
 Lemma divide_mul_r : forall n m p, (n | p) -> (n | m * p).
@@ -172,13 +180,13 @@ Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m.
 Proof.
  intros n m Hm (q,Hq).
  destruct (le_gt_cases n 0) as [Hn|Hn]. order.
- rewrite <- Hq.
+ rewrite Hq.
  destruct (lt_ge_cases q 0) as [Hq'|Hq'].
- generalize (mul_pos_neg n q Hn Hq'). order.
+ generalize (mul_neg_pos q n Hq' Hn). order.
  le_elim Hq'.
- rewrite <- (mul_1_r n) at 1. apply mul_le_mono_pos_l; trivial.
+ rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial.
  now rewrite one_succ, le_succ_l.
- rewrite <- Hq', mul_0_r in Hq. order.
+ rewrite <- Hq', mul_0_l in Hq. order.
 Qed.
 
 (** Basic properties of gcd *)
@@ -291,8 +299,8 @@ Qed.
 
 Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n).
 Proof.
- intros n m Hn. split. intros (q,Hq). rewrite <- Hq.
- now apply gcd_mul_diag_l.
+ intros n m Hn. split. intros (q,Hq). rewrite Hq.
+ rewrite mul_comm. now apply gcd_mul_diag_l.
  intros EQ. rewrite <- EQ. apply gcd_divide_r.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v
index 1192e5cdc..ece369d80 100644
--- a/theories/Numbers/Natural/Abstract/NGcd.v
+++ b/theories/Numbers/Natural/Abstract/NGcd.v
@@ -27,7 +27,7 @@ Definition divide_antisym n m : (n | m) -> (m | n) -> n == m
 Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p).
 Proof.
  intros n m p (q,Hq) (r,Hr).
- exists (r-q). rewrite mul_sub_distr_l, Hq, Hr.
+ exists (r-q). rewrite mul_sub_distr_r, <- Hq, <- Hr.
  now rewrite add_comm, add_sub.
 Qed.
 
@@ -194,15 +194,15 @@ Proof.
  assert (G := gcd_nonneg n m). le_elim G.
  destruct (gcd_divide_l n m) as (q,Hq).
  exists (gcd n m). exists q.
- split. easy.
+ split. now rewrite mul_comm.
  split. apply gcd_divide_r.
  destruct (gcd_divide_r n m) as (r,Hr).
- rewrite <- Hr in H. rewrite <- Hq in H at 1.
- rewrite <- mul_assoc in H. apply mul_divide_cancel_l in H; [|order].
+ rewrite Hr in H. rewrite Hq in H at 1.
+ rewrite mul_shuffle0 in H. apply mul_divide_cancel_r in H; [|order].
  apply gauss with r; trivial.
- apply mul_cancel_l with (gcd n m); [order|].
- rewrite mul_1_r.
- rewrite <- gcd_mul_mono_l, Hq, Hr; order.
+ apply mul_cancel_r with (gcd n m); [order|].
+ rewrite mul_1_l.
+ rewrite <- gcd_mul_mono_r, <- Hq, <- Hr; order.
  symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v
index 321508f58..1e8e678c6 100644
--- a/theories/Numbers/Natural/Abstract/NLcm.v
+++ b/theories/Numbers/Natural/Abstract/NLcm.v
@@ -30,9 +30,9 @@ Module Type NLcmProp
 Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)).
 Proof.
  intros a b Hb. split.
- intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2.
-  rewrite Hab; now nzsimpl.
- intros (c,Hc). rewrite <- Hc, mul_comm. now apply mod_mul.
+ intros Hab. exists (a/b). rewrite mul_comm.
+  rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl.
+ intros (c,Hc). rewrite Hc. now apply mod_mul.
 Qed.
 
 Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) ->
@@ -132,7 +132,7 @@ Qed.
 Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a).
 Proof.
  intros a b c Ha Hb (c',Hc). exists c'.
- now rewrite mul_comm, <- divide_div_mul_exact, mul_comm, Hc.
+ now rewrite <- divide_div_mul_exact, Hc.
 Qed.
 
 Lemma lcm_least : forall a b c,
@@ -146,14 +146,14 @@ Proof.
  set (g:=gcd a b) in *.
  assert (Ha' := divide_div g a c NEQ Ga Ha).
  assert (Hb' := divide_div g b c NEQ Gb Hb).
- destruct Ha' as (a',Ha'). rewrite <- Ha' in Hb'.
+ destruct Ha' as (a',Ha'). rewrite Ha', mul_comm in Hb'.
  apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm].
  destruct Hb' as (b',Hb').
  exists b'.
- rewrite <- mul_assoc, Hb'.
+ rewrite mul_shuffle3, <- Hb'.
  rewrite (proj2 (div_exact c g NEQ)).
- rewrite <- Ha', mul_assoc. f_equiv.
- apply div_exact; trivial.
+ rewrite Ha', mul_shuffle3, (mul_comm a a'). f_equiv.
+ symmetry. apply div_exact; trivial.
  apply mod_divide; trivial.
  apply mod_divide; trivial. transitivity a; trivial.
 Qed.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 8a26ec6e3..b6b26363e 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -343,7 +343,7 @@ Fixpoint gcd a b :=
    | S a' => gcd (b mod (S a')) (S a')
   end.
 
-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) : nat_scope.
 
 Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
@@ -351,17 +351,18 @@ Proof.
  fix 1.
  intros [|a] b; simpl.
  split.
-  exists 0; now rewrite <- mult_n_O.
-  exists 1; now rewrite <- mult_n_Sm, <- mult_n_O.
+  now exists 0.
+  exists 1. simpl. now rewrite <- plus_n_O.
  fold (b mod (S a)).
  destruct (gcd_divide (b mod (S a)) (S a)) as (H,H').
  set (a':=S a) in *.
  split; auto.
  rewrite (div_mod b a') at 2 by discriminate.
  destruct H as (u,Hu), H' as (v,Hv).
+ rewrite mult_comm.
  exists ((b/a')*v + u).
- rewrite mult_plus_distr_l.
- now rewrite (mult_comm _ v), mult_assoc, Hv, Hu.
+ rewrite mult_plus_distr_r.
+ now rewrite <- mult_assoc, <- Hv, <- Hu.
 Qed.
 
 Lemma gcd_divide_l : forall a b, (gcd a b | a).
@@ -383,8 +384,9 @@ Proof.
  set (a':=S a) in *.
  rewrite (div_mod b a') in H' by discriminate.
  destruct H as (u,Hu), H' as (v,Hv).
- exists (v - u * (b/a')).
- now rewrite mult_minus_distr_l, mult_assoc, Hu, Hv, minus_plus.
+ exists (v - (b/a')*u).
+ rewrite mult_comm in Hv.
+ now rewrite mult_minus_distr_r, <- Hv, <-mult_assoc, <-Hu, minus_plus.
 Qed.
 
 (** * Bitwise operations *)
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 878e46fea..33181e32a 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -331,7 +331,7 @@ Qed.
 
 (** Gcd *)
 
-Definition divide n m := exists p, n*p == m.
+Definition divide n m := exists p, m == p*n.
 Local Notation "( x | y )" := (divide x y) (at level 0).
 
 Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m].
@@ -341,8 +341,8 @@ Proof.
  intros (z,H). exists (of_N (Zabs_N z)). zify.
  rewrite Z_of_N_abs.
  rewrite <- (Zabs_eq [n]) by apply spec_pos.
- rewrite <- Zabs_Zmult, H.
- apply Zabs_eq, spec_pos.
+ rewrite <- Zabs_Zmult, <- H.
+ symmetry. apply Zabs_eq, spec_pos.
 Qed.
 
 Lemma gcd_divide_l : forall n m, (gcd n m | n).