def fits_sub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:69

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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

69def fits_sub(+k: Nat, +x: Nat, +y: Nat, +hx: {C.fits(k, x) == True{} : Bool}) -> {C.fits(k, Nat.sub(x, y)) == True{} : Bool}:
70  WW.fits_of_lt(k, Nat.sub(x, y), N.le_lt_trans(Nat.sub(x, y), x, C.pow2(k), AR.sub_le2(x, y), WW.lt_of_fits(k, x, hx)))