diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-06 09:03:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-06 09:03:53 +0000 |
| commit | 82791d73beaaeee5eab1fec317c689deb29f0a49 (patch) | |
| tree | 05900af4d5e8090255f0a348c1e043bb00e68e9e /theories/Numbers/Integer/Abstract/ZDivEucl.v | |
| parent | 70eb4b8dd94ef17cb246a25eb7525626e0f30296 (diff) | |
"by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... by ...")
Application in some proofs of Numbers's abstract division
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12630 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZDivEucl.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index a853395a6..914055654 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -385,7 +385,7 @@ nzsimpl. rewrite (add_lt_mono_r _ _ (a mod c)). rewrite <- div_mod by order. apply lt_le_trans with b; trivial. -rewrite (div_mod b c) at 1; [| order]. +rewrite (div_mod b c) at 1 by order. rewrite <- add_assoc, <- add_le_mono_l. apply le_trans with (c+0). nzsimpl; destruct (mod_always_pos b c); try order. @@ -524,7 +524,7 @@ rewrite abs_mul, (abs_pos c) by order. rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial. apply mod_always_pos. (* equation *) -rewrite (div_mod a b) at 1; [|order]. +rewrite (div_mod a b) at 1 by order. rewrite mul_add_distr_r. rewrite add_cancel_r. rewrite <- 2 mul_assoc. now rewrite (mul_comm c). @@ -568,7 +568,7 @@ Lemma mul_mod_idemp_l : forall a b n, n~=0 -> ((a mod n)*b) mod n == (a*b) mod n. Proof. intros a b n Hn. symmetry. - rewrite (div_mod a n) at 1; [|order]. + rewrite (div_mod a n) at 1 by order. rewrite add_comm, (mul_comm n), (mul_comm _ b). rewrite mul_add_distr_l, mul_assoc. rewrite mod_add by trivial. @@ -591,7 +591,7 @@ Lemma add_mod_idemp_l : forall a b n, n~=0 -> ((a mod n)+b) mod n == (a+b) mod n. Proof. intros a b n Hn. symmetry. - rewrite (div_mod a n) at 1; [|order]. + rewrite (div_mod a n) at 1 by order. rewrite <- add_assoc, add_comm, mul_comm. now rewrite mod_add. Qed. @@ -628,7 +628,7 @@ Proof. rewrite (abs_pos b) by order. now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l. (* end 0<= ... < abs(b*c) *) - rewrite (div_mod a b) at 1; [|order]. + rewrite (div_mod a b) at 1 by order. rewrite add_assoc, add_cancel_r. rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. apply div_mod; order. |