Uint64n.neg_sum: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
Lines 63-73 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&start_line=63&end_line=73

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/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend as M128

# a nonzero word and its negation add up to 2^64
def neg_sum(+one: Nat, +h1: {one == 1n : Nat}, +n: WU.U64, +hn: {Nat.is_eq(SW.value(n), 0n) == False{} : Bool}) -> {Nat.add(SW.value(X.sub(Z(), n)), SW.value(n)) == C.shift(64n, one) : Nat}:
  +s = SW.value(X.sub(Z(), n))
  +vn = SW.value(n)
  +q = M128.QSUB(one, Z(), n)
  +e = M128.sub_eq(one, h1, Z(), n)
  +hs = Equal.trans(Bool, C.fits(65n, C.shift(64n, q)), C.fits(65n, Nat.add(s, vn)), True{}, Equal.cong(Nat, Bool, z => C.fits(65n, z), C.shift(64n, q), Nat.add(s, vn), Equal.sym(Nat, Nat.add(s, vn), C.shift(64n, q), e)), M128.sum_fits(64n, s, vn, M128.fit64(X.sub(Z(), n)), M128.fit64(n)))
  +hq1 = Equal.trans(Bool, C.fits(1n, q), C.fits(1n, C.high(64n, C.shift(64n, q))), True{}, Equal.cong(Nat, Bool, z => C.fits(1n, z), q, C.high(64n, C.shift(64n, q)), Equal.sym(Nat, C.high(64n, C.shift(64n, q)), q, WI.high_u(64n, 0n, q, {==}))), M128.fits_hi(C.shift(64n, q), hs))
  +hq = q_nz(q, s, vn, hn, e)
  %q_one(q, one, h1, Nat.is_eq(q, 0n), {==}, hq, hq1) : {Nat.add(s, vn) == C.shift(64n, _) : Nat}
  e

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.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_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=Z
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=q_nz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=q_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend&name=QSUB
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend&name=fit64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend&name=fits_hi
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend&name=sub_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend&name=sum_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=high_u
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=high
  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/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=sub