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 32ae4dde7..194f94385 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -95,7 +95,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. @@ -103,7 +103,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_old : exists x, (x * x = a)%GF. |