Negate.comp1_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend as Negate
Lines 84-98 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&start_line=84&end_line=98

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/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

# comp1(x) + x + 1 = 2^16 for x < 2^16
def comp1_v(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), 1n) == C.shift(16n, one) : Nat}:
  +lo = Nat.mod(x, 256n)
  +hi = Nat.div(x, 256n)
  +hl = N.lt_succ_le(lo, 255n, NR.dm_lt(255n, x))
  +hh = N.lt_succ_le(hi, 255n, hi_byte_lt(one, h1, x, hx))
  %Equal.sym(Nat, x, Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)) : {Nat.add(Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), _), 1n) == C.shift(16n, one) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n))), Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 256n)), combine(Nat.sub(255n, Nat.mod(x, 256n)), Nat.sub(255n, Nat.div(x, 256n)), Nat.div(x, 256n), Nat.mod(x, 256n), 256n)) : {Nat.add(_, 1n) == C.shift(16n, one) : Nat}
  %Equal.sym(Nat, 256n, C.shift(8n, one), Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1))) : {Nat.add(Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), _)), 1n) == C.shift(16n, one) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), 255n, N.sub_add(255n, Nat.mod(x, 256n), hl)) : {Nat.add(Nat.add(_, Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 255n, N.sub_add(255n, Nat.div(x, 256n), hh)) : {Nat.add(Nat.add(255n, Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(_, Nat.mul(255n, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(Nat.sub(C.shift(8n, one), 1n), C.shift(8n, one))), 1n), Nat.mul(C.shift(8n, one), C.shift(8n, one)), digit_max(C.shift(8n, one), bb_pos(one, h1))) : {_ == C.shift(16n, one) : Nat}
  bb_sq(one, h1)

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=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  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/limbs.bend&name=b8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=bb_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=bb_sq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=combine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=digit_max
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=e255
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=hi_byte_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=comp1