diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-05 19:04:28 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-06 11:20:59 -0400 |
| commit | de58a46d929f334fc20ae0a63ddbdf867d3fb9fc (patch) | |
| tree | a8c0d58ebf795307b7f4d179200256d1ac19082c /src/ModularArithmetic | |
| parent | ebb83ddb57aa8da5dbaae11de69c2fdc1a3e8c97 (diff) | |
Finished sqrt in GF25519
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 878b62abe..2d4bb525f 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -991,8 +991,6 @@ Section SquareRoots. etransitivity. Focus 2. { apply if_equiv. { - etransitivity. - Focus 2. { apply eqb_Proper; [ | reflexivity ]. transitivity (carry_mul_opt k_ c_ (pow_opt k_ c_ one_ us chain) (pow_opt k_ c_ one_ us chain)); [ reflexivity | ]. cbv [eq]. @@ -1000,11 +998,6 @@ Section SquareRoots. rewrite carry_mul_rep by reflexivity. rewrite mul_rep by reflexivity. f_equal; apply pow_opt_correct; auto. - } Unfocus. - cbv [ModularBaseSystem.eqb freeze]. - rewrite <-!from_list_default_eq with (d := 0). - erewrite <-!freeze_opt_correct by eauto using length_to_list. - reflexivity. } { apply pow_opt_correct; auto. } { |