diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-25 17:37:05 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-04-25 17:37:05 -0400 |
| commit | 593691bb1f3dd6835329f0221d3bc71d3f318aae (patch) | |
| tree | 2f4ce94c7261feec8f7a3ec95ac7a04635eada35 /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | 2590c4a391038e5a682105ebbf4eb7c307f7b6b0 (diff) | |
refactor field lemmas out of ed25519
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 130f85c84..759085dc6 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -249,6 +249,16 @@ Section VariousModPrime. intros; field. (* TODO: Warning: Collision between bound variables ... *) Qed. + Lemma F_inv_0 : inv 0 = (0 : F q). + Proof. + destruct (@F_inv_spec q); auto. + Qed. + + Lemma F_div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F. + Proof. + intros; destruct (F_eq_dec y 0); [subst;unfold div;rewrite !F_inv_0|]; field. + Qed. + Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0). Proof. split; intro A. |