def limbs_fit

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:231

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

231# r fits k bits, x fits j bits: r + shift(k, x) fits k + j bits
232def limbs_fit(+k: Nat, +j: Nat, +r: Nat, +x: Nat, +hr: {C.fits(k, r) == True{} : Bool}, +hx: {C.fits(j, x) == True{} : Bool}) -> {C.fits(Nat.add(k, j), Nat.add(r, C.shift(k, x))) == True{} : Bool}:
233  fits_of_lt(Nat.add(k, j), Nat.add(r, C.shift(k, x)), two_limb_lt(k, j, r, x, lt_of_fits(k, r, hr), lt_of_fits(j, x, hx)))