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

2 files changed, 15 insertions, 15 deletions

diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v
index 1192e5cdc6..ece369d804 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 321508f584..1e8e678c64 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.