diff options
Diffstat (limited to 'src/Specific/GF25519BoundedExtendedAddCoordinates.v')
| -rw-r--r-- | src/Specific/GF25519BoundedExtendedAddCoordinates.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/Specific/GF25519BoundedExtendedAddCoordinates.v b/src/Specific/GF25519BoundedExtendedAddCoordinates.v index 3910edab8..cb42b9e7f 100644 --- a/src/Specific/GF25519BoundedExtendedAddCoordinates.v +++ b/src/Specific/GF25519BoundedExtendedAddCoordinates.v @@ -41,12 +41,19 @@ Proof. end. Qed. -Definition add_coordinates twice_d P1 P2 +Definition add_coordinates' twice_d P1 P2 := let '(P10, P11, P12, P13) := P1 in let '(P20, P21, P22, P23) := P2 in @GF25519BoundedAddCoordinates.add_coordinates twice_d P10 P11 P12 P13 P20 P21 P22 P23. +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF25519BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF25519BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + Lemma add_coordinates_correct_full twice_d P1 P2 : Tuple.fieldwise GF25519BoundedCommon.eq |