def unfit_big

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

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

954# an unfit value is >= 1, so the mode is the >= 1 one
955def unfit_big(+x: Nat, +md: Bool, +hm: {mode(md, x) == True{} : Bool}, +hx: {C.fits(32n, x) == False{} : Bool}) -> {md == True{} : Bool}:
956  match md:
957    case True{}:
958      {==}
959    case False{}:
960      Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, x), False{}, Equal.sym(Bool, C.fits(32n, x), True{}, small_fits(x, hm)), hx)))