def high_pos

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64clz.bend:65

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

65# 2^k <= y: high(k, y) >= 1
66def high_pos(+k: Nat, +y: Nat, +h: {Nat.is_le(C.pow2(k), y) == True{} : Bool}) -> {Nat.is_le(1n, C.high(k, y)) == True{} : Bool}:
67  hp_c(k, y, h, C.high(k, y), {==})