Listops.uniq_lo: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend as Listops
Lines 106-111 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&start_line=106&end_line=111

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

def uniq_lo(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +e: {Nat.add(x, C.shift(16n, a)) == Nat.add(y, C.shift(16n, b)) : Nat}) -> {x == y : Nat}:
  +wp = Nat.sub(C.shift(16n, one), 1n)
  +ex = Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), x, NR.mod_of(a, wp, x, lt_w(one, h1, x, hx)))
  +ey = NR.mod_of(b, wp, y, lt_w(one, h1, y, hy))
  +e2 = Equal.trans(Nat, Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(b, 1n+wp), y), Equal.sym(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(a, 1n+wp), x), digit_form(one, h1, x, a)), Equal.trans(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), Nat.add(Nat.mul(b, 1n+wp), y), e, digit_form(one, h1, y, b)))
  Equal.trans(Nat, x, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), y, ex, Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), Nat.mod(Nat.add(Nat.mul(b, 1n+wp), y), 1n+wp), y, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+wp), Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(Nat.mul(b, 1n+wp), y), e2), ey))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&name=digit_form
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&name=lt_w
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=mod_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift