def unfit_nz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:383

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/logic.bend as L

383# a nonzero multiple of 2^k added: does not fit k bits
384def unfit_nz(+k: Nat, +r: Nat, +q: Nat, +hq: {Nat.is_eq(q, 0n) == False{} : Bool}) -> {C.fits(k, Nat.add(r, C.shift(k, q))) == False{} : Bool}:
385  match q:
386    case 0n:
387      Empty.absurd({C.fits(k, Nat.add(r, C.shift(k, 0n))) == False{} : Bool}, L.false_true(Equal.sym(Bool, True{}, False{}, hq)))
388    case 1n+ +qp:
389      unfit_shift(k, r, qp)