def fits_mono

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sh.bend:129

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

129def fits_mono(+a: Nat, +b: Nat, +x: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +h: {C.fits(a, x) == True{} : Bool}) -> {C.fits(b, x) == True{} : Bool}:
130  WW.fits_of_lt(b, x, N.lt_le_trans(x, C.pow2(a), C.pow2(b), WW.lt_of_fits(a, x, h), N.pow2_mono(a, b, hab)))