~/jendhub

def high_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/below.bend:60

import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend as Below
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

60# x < 2^64 and n > 0: floor(x n / 2^64) < n
61def 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}:
62  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)

Used by (2)