def byte_lt
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:168
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/u32and.bend as FB
168def byte_lt(+b: U32) -> {Nat.is_lt(B.byte(b), 256n) == True{} : Bool}:
169 %Equal.sym(Nat, U32.to_nat(U32.and(b, 255)), C.low(8n, U32.to_nat(b)), FB.andm(b, 8n, 255, {==})) : {Nat.is_lt(_, 256n) == True{} : Bool}
170 WW.low_lt(8n, U32.to_nat(b))