U64.negative_pack: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as U64
Lines 94-101 of bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&start_line=94&end_line=101

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

# The sign of the 64-bit word is the top bit of the high limb.
def negative_pack(+lo: U32, +hi: U32) -> {S.negative(W.pack(lo, hi)) == U32.is_ge(hi, 2147483648) : Bool}:
  match lo hi:
    case U32{a} U32{b}:
      %Equal.sym(Word(64n), W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n)), S.sign_threshold(63n), threshold()) : {Cmp.is_ge(Word.cmp(64n, W.join(32n, 32n, a, b), _)) == U32.is_ge(U32{b}, 2147483648) : Bool}
      %Equal.sym(Cmp, Word.cmp(64n, W.join(32n, 32n, a, b), W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n))), U.order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n))), cmp_join(32n, 32n, a, b, Word.zero(32n), S.sign_threshold(31n))) : {Cmp.is_ge(_) == U32.is_ge(U32{b}, 2147483648) : Bool}
      %Equal.sym(U32, U32{S.sign_threshold(31n)}, 2147483648, threshold_u32()) : {Cmp.is_ge(U.order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n)))) == U32.is_ge(U32{b}, _) : Bool}
      ge_order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n)), ge_zero(32n, a))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_ge
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_ge
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=negative
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=sign_threshold
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=join
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=cmp_join
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=ge_order
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=ge_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=threshold
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=threshold_u32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=order