Bytes.le_below: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend as Bytes
Lines 190-201 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&start_line=190&end_line=201

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

def le_below(+x: W.U64) -> {SCR.below256(SCR.le_bytes(x)) == True{} : Bool}:
  match x:
    case W.U64{+l, +h}:
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 0n), 256), True{}, byte_of_lt(l, 0n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 8n), SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 8n), 256), True{}, byte_of_lt(l, 8n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 16n), SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 16n), 256), True{}, byte_of_lt(l, 16n)) : {Bool.and(_, SCR.below256([SCR.byte_of(l, 24n), SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(l, 24n), 256), True{}, byte_of_lt(l, 24n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 0n), SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 0n), 256), True{}, byte_of_lt(h, 0n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 8n), SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 8n), 256), True{}, byte_of_lt(h, 8n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 16n), SCR.byte_of(h, 24n)])) == True{} : Bool}
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 16n), 256), True{}, byte_of_lt(h, 16n)) : {Bool.and(_, SCR.below256([SCR.byte_of(h, 24n)])) == True{} : Bool}
      %Equal.sym(Bool, U32.is_lt(SCR.byte_of(h, 24n), 256), True{}, byte_of_lt(h, 24n)) : {Bool.and(_, True{}) == True{} : Bool}
      {==}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=byte_of_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=below256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=byte_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=le_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend&name=U64