diff options
Diffstat (limited to 'src/Specific/EdDSA25519.v')
| -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. |