Paff.aff_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as Paff
Lines 38-49 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&start_line=38&end_line=49

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/field.bend as F
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/fieldops.bend as FO
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as FP
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT

# (X / Z, Y / Z)
def aff_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, +ha: {PT.pred(one, a) == True{} : Bool}) -> {av(one, P.to_affine(a)) == CV.to_affine(FS.prime(one), PT.pv(one, a)) : CV.SAffine}:
  match a:
    case P.Point{+x, +y, +z}:
      +hx = rx(one, x, y, z, ha)
      +hy = ry(one, x, y, z, ha)
      +hz = rz(one, x, y, z, ha)
      %Equal.sym(Nat, FS.value(one, F.mul(x, F.inv(z))), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, F.inv(z))), FO.mul_v(one, h1, x, F.inv(z), hx, FP.inv_r(one, h1, z, hz))) : {CV.SAffine{_, FS.value(one, F.mul(y, F.inv(z)))} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
      %Equal.sym(Nat, FS.value(one, F.mul(y, F.inv(z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, F.inv(z))), FO.mul_v(one, h1, y, F.inv(z), hy, FP.inv_r(one, h1, z, hz))) : {CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, F.inv(z))), _} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
      %Equal.sym(Nat, FS.value(one, F.inv(z)), FS.minv(FS.prime(one), FS.value(one, z)), FP.inv_v(one, h1, z, hz)) : {CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), _), FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, F.inv(z)))} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
      %Equal.sym(Nat, FS.value(one, F.inv(z)), FS.minv(FS.prime(one), FS.value(one, z)), FP.inv_v(one, h1, z, hz)) : {CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), _)} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
      {==}

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend&name=mul_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&name=inv_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&name=inv_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=av
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=rx
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=ry
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=rz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=pred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=pv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=SAffine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=to_affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=minv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=mmul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=prime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend&name=inv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend&name=mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=Point
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=to_affine