diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-01-13 12:19:14 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-01-13 12:19:14 -0500 |
| commit | 97cd9a342824b3d6ceac707ca1aab5e552075b3f (patch) | |
| tree | 030d14a47bc31123686d0e09ed5e67c8b106e579 /src/Specific | |
| parent | 71553f59573301744c7d34aeec6a371ee50a65cf (diff) | |
euler's criterion reduced to fermat's little theorem and two lemmas about primitive roots.
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/EdDSA25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index 26c45a713..f5546f3c8 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -94,7 +94,7 @@ Module EdDSA25519_Params <: EdDSAParams. Qed. Lemma square_mod_GF : forall (a x : Z), - (0 <= x < q /\ x * x mod q = a)%Z -> + (x * x mod q = a)%Z -> (inject x * inject x = inject a)%GF. Proof. intros. @@ -102,7 +102,7 @@ Module EdDSA25519_Params <: EdDSAParams. rewrite <- inject_distr_mul. rewrite inject_mod_eq. replace modulus with q by auto. - rewrite H1; reflexivity. + reflexivity. Qed. Lemma a_square : exists x, (x * x = a)%GF. |