Below.high_lt_c: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend as Below
Lines 34-44 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend&start_line=34&end_line=44

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/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
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/random/lemire.bend as LE

# x < 2^64 and n > 0: floor(x n / 2^64) < n
def high_lt_c(+x: Nat, +n: Nat, +y: Nat, +hy: {Nat.is_lt(y, C.shift(64n, n)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(C.high(64n, y), n) == c : Bool}) -> {c == True{} : Bool}:
  match c:
    case True{}:
      {==}
    case False{}:
      +h = C.high(64n, y)
      +ge = N.le_trans(C.shift(64n, n), C.shift(64n, h), y, WI.shift_mono(64n, n, h, N.not_lt_le(h, n, hc)),
        %Equal.sym(Nat, y, Nat.add(C.low(64n, y), C.shift(64n, h)), WI.low_high(64n, y)) : {Nat.is_le(C.shift(64n, h), _) == True{} : Bool}
        LE.le_plus(C.low(64n, y), C.shift(64n, h)))
      Empty.absurd({False{} == True{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_lt(y, C.shift(64n, n)), True{}, Equal.sym(Bool, Nat.is_lt(y, C.shift(64n, n)), False{}, N.le_not_lt(y, C.shift(64n, n), ge)), hy)))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_not_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend&name=le_plus
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=low_high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_mono
  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=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift