def uniq_lo

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:106

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

106def 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}:
107  +wp = Nat.sub(C.shift(16n, one), 1n)
108  +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)))
109  +ey = NR.mod_of(b, wp, y, lt_w(one, h1, y, hy))
110  +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)))
111  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))