def unfit_big

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:955

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

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