diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-03-03 16:17:42 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:42:16 -0400 |
| commit | fcd17b377f948b15eec9e23cc15bb6dffb411118 (patch) | |
| tree | 3de8cebdc7f363b09cae653cc215e89100ccba31 /src | |
| parent | 4fa76e9d403d0d4f7ce8969acbe9612aa8fc3f56 (diff) | |
tweak to NumTheoryUtil so it builds on older Coq versions
Diffstat (limited to 'src')
| -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. |