def byte_lt1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:172

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/crypto/secp256k1/limbs.bend as LV

172def byte_lt1(+one: Nat, +h1: {one == 1n : Nat}, +b: U32) -> {Nat.is_lt(B.byte(b), C.shift(8n, one)) == True{} : Bool}:
173  %Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1)) : {Nat.is_lt(B.byte(b), _) == True{} : Bool}
174  byte_lt(b)