Below.high_lt: 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 60-62 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=60&end_line=62

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

# x < 2^64 and n > 0: floor(x n / 2^64) < n
def high_lt(+x: Nat, +n: Nat, +hx: {C.fits(64n, x) == True{} : Bool}, +hn: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(C.high(64n, Nat.mul(x, n)), n) == True{} : Bool}:
  high_lt_c(x, n, Nat.mul(x, n), prod_lt(x, n, 1n, {==}, hx, hn), Nat.is_lt(C.high(64n, Nat.mul(x, n)), n), {==})

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend&name=high_lt_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend&name=prod_lt
  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