Sel.psel1: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as Sel
Lines 102-108 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&start_line=102&end_line=108

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
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/point.bend as PT

def psel1(+one: Nat, a: P.Point, b: P.Point, +ha: {PT.pred(one, a) == True{} : Bool}, +hb: {PT.pred(one, b) == True{} : Bool}) -> {P.select(1n, a, b) == a : P.Point}:
  match a b:
    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
      %Equal.sym(List<&2, Nat>, L.select(1n, x1, x2), x1, sel1(one, 16n, x1, x2, rx(one, x1, y1, z1, ha), rx(one, x2, y2, z2, hb))) : {P.Point{_, L.select(1n, y1, y2), L.select(1n, z1, z2)} == P.Point{x1, y1, z1} : P.Point}
      %Equal.sym(List<&2, Nat>, L.select(1n, y1, y2), y1, sel1(one, 16n, y1, y2, ry(one, x1, y1, z1, ha), ry(one, x2, y2, z2, hb))) : {P.Point{x1, _, L.select(1n, z1, z2)} == P.Point{x1, y1, z1} : P.Point}
      %Equal.sym(List<&2, Nat>, L.select(1n, z1, z2), z1, sel1(one, 16n, z1, z2, rz(one, x1, y1, z1, ha), rz(one, x2, y2, z2, hb))) : {P.Point{x1, y1, _} == P.Point{x1, y1, z1} : P.Point}
      {==}

Uses (12):
  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=List
  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/point.bend&name=pred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=rx
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=ry
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=rz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=sel1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=select
  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=select