diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-15 14:36:54 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-15 15:04:40 -0500 |
| commit | ff2eb39f8c33b83d3c6a8ddf029bbff96626e429 (patch) | |
| tree | 36c2cb159f5133a0cd4942d85deacbda7a1e7e84 /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | 949d85496b76c22931cf3aa975b7b719beb6c200 (diff) | |
| parent | 4b0a55cf320ade4ac8333f9feafbac1b3288bd54 (diff) | |
Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec
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 6594ae4ed..2f548935f 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -286,7 +286,7 @@ Section SquareRootsPrime5Mod8. (* This is only the square root of -1 if q mod 8 is 3 or 5 *) Definition sqrt_minus1 : F q := ZToField 2 ^ Z.to_N (q / 4). - Lemma two_lt_q : 2 < q. + Lemma two_lt_q_5mod8 : 2 < q. Proof. pose proof (prime_ge_2 q _) as two_le_q. apply Zle_lt_or_eq in two_le_q. @@ -342,7 +342,7 @@ Section SquareRootsPrime5Mod8. replace (Z.to_N 2) with 2%N by auto. ring. - symmetry; apply euler_criterion_F; auto using two_lt_q. + symmetry; apply euler_criterion_F; auto using two_lt_q_5mod8. } Qed. |