def low_u

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

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

222def low_u(+k: Nat, +r: Nat, +q: Nat, +hr: {C.fits(k, r) == True{} : Bool}) -> {C.low(k, Nat.add(r, C.shift(k, q))) == r : Nat}:
223  low_uniq(k, r, q, lt_of_fits(k, r, hr))