def fits_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/random/wrappers.bend:150

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

150# x < 2^k gives x 2^a < 2^(a + k)
151def fits_shift(+a: Nat, +k: Nat, +x: Nat, +h: {C.fits(k, x) == True{} : Bool}) -> {C.fits(Nat.add(a, k), C.shift(a, x)) == True{} : Bool}:
152  WW.limbs_fit(a, k, 0n, x, fits0(a), h)