def fits_lek

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64m128.bend:72

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/math/typed/width.bend as WW

72def fits_lek(+k: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(x, y) == True{} : Bool}, +hy: {C.fits(k, y) == True{} : Bool}) -> {C.fits(k, x) == True{} : Bool}:
73  WW.fits_of_lt(k, x, N.le_lt_trans(x, y, C.pow2(k), h, WW.lt_of_fits(k, y, hy)))