Sel.psel0: 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 93-100 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=93&end_line=100

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

# b = 0 picks the second point, b = 1 the first
def psel0(+one: Nat, a: P.Point, b: P.Point, +ha: {PT.pred(one, a) == True{} : Bool}, +hb: {PT.pred(one, b) == True{} : Bool}) -> {P.select(0n, a, b) == b : P.Point}:
  match a b:
    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
      %Equal.sym(List<&2, Nat>, L.select(0n, x1, x2), x2, sel0(one, 16n, x1, x2, rx(one, x1, y1, z1, ha), rx(one, x2, y2, z2, hb))) : {P.Point{_, L.select(0n, y1, y2), L.select(0n, z1, z2)} == P.Point{x2, y2, z2} : P.Point}
      %Equal.sym(List<&2, Nat>, L.select(0n, y1, y2), y2, sel0(one, 16n, y1, y2, ry(one, x1, y1, z1, ha), ry(one, x2, y2, z2, hb))) : {P.Point{x2, _, L.select(0n, z1, z2)} == P.Point{x2, y2, z2} : P.Point}
      %Equal.sym(List<&2, Nat>, L.select(0n, z1, z2), z2, sel0(one, 16n, z1, z2, rz(one, x1, y1, z1, ha), rz(one, x2, y2, z2, hb))) : {P.Point{x2, y2, _} == P.Point{x2, y2, z2} : 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=sel0
  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