def unfit_mono

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:351

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

351# a value that does not fit stays unfit when it grows
352def unfit_mono(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}, +hf: {C.fits(k, a) == False{} : Bool}) -> {C.fits(k, b) == False{} : Bool}:
353  +na = Equal.trans(Bool, Nat.is_lt(a, C.pow2(k)), C.fits(k, a), False{}, Equal.sym(Bool, C.fits(k, a), Nat.is_lt(a, C.pow2(k)), WW.fits_lt(k, a)), hf)
354  Equal.trans(Bool, C.fits(k, b), Nat.is_lt(b, C.pow2(k)), False{}, WW.fits_lt(k, b), N.le_not_lt(b, C.pow2(k), N.le_trans(C.pow2(k), a, b, N.not_lt_le(a, C.pow2(k), na), h)))