diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-02 12:08:02 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-02 12:18:52 -0700 |
| commit | cd6c4f1297a6604fa4691a5f13808b721194f13b (patch) | |
| tree | 71075b2573818cae036f87a7efda7f3372eb4e3e /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | 2939418894d78c095cd9142ce99c615f2d61dda6 (diff) | |
Make ZUtil more uniform
The standard library uses Z.*, and Z* and Z_* are compatibility
notations. We follow suit.
Also, eliminate a few lemmas that are duplicates of ones in the standard
library.
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2021e8514..a2f606f30 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -460,8 +460,8 @@ Section SquareRootsPrime5Mod8. apply Z2N.inj_iff; try zero_bounds. rewrite <- Z.mul_cancel_l with (p := 2) by omega. ring_simplify. - rewrite mul_div_eq by omega. - rewrite mul_div_eq by omega. + rewrite Z.mul_div_eq by omega. + rewrite Z.mul_div_eq by omega. rewrite (Zmod_div_mod 2 8 q) by (try omega; apply Zmod_divide; omega || auto). rewrite q_5mod8. |