diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-03-03 16:17:42 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-03-03 16:17:42 -0500 |
| commit | 904e5e649010ff08b28be7560365c018bd683eef (patch) | |
| tree | 2b2178d7b4f86934983e8a1f5367522e976e34f3 /src/Util/NumTheoryUtil.v | |
| parent | 2fa2df7f86b39edfb6d817954c1a5332c4e1a431 (diff) | |
tweak to NumTheoryUtil so it builds on older Coq versions
Diffstat (limited to 'src/Util/NumTheoryUtil.v')
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 190fd5274..5acef8b75 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -100,7 +100,7 @@ Proof. pose proof (prime_ge_2 _ prime_p). rewrite Zmult_mod_idemp_r. replace (a * a ^ (p - 2)) with (a^(p-1)). - 2:replace a with (a^1) at 2 by ring. + 2:replace (a * a ^ (p - 2)) with (a^1 * a ^ (p - 2)) by ring. 2:rewrite <-Zpower_exp; try f_equal; omega. auto using fermat_little. Qed. |