def aff_x_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pver.bend:27

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

27def aff_x_v(+one: Nat, a: P.Affine) -> {FS.value(one, P.aff_x(a)) == CV.aff_x(PA.av(one, a)) : Nat}:
28  match a:
29    case P.Affine{x, y}:
30      {==}