Bytes.fits_one: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
Lines 232-242 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&start_line=232&end_line=242

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/proofs/lib/nat.bend as N
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/ineq.bend as I

# x < 2^k (2^k with a symbolic one): x fits k bits
def fits_one(k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(k, one)) == True{} : Bool}) -> {C.fits(k, x) == True{} : Bool}:
  match k:
    case 0n:
      +hx1 = I.lt_subst_r(x, one, 1n, h1, hx)
      +e0 = N.le_antisym(x, 0n, N.lt_succ_le(x, 0n, hx1), N.zero_le(x))
      %Equal.sym(Nat, x, 0n, e0) : {Nat.is_eq(_, 0n) == True{} : Bool}
      {==}
    case 1n+ +j:
      +hh = Equal.trans(Bool, Nat.is_lt(C.half(x), C.shift(j, one)), Nat.is_lt(x, Nat.double(C.shift(j, one))), True{}, WW.lt_half(x, C.shift(j, one)), hx)
      fits_one(j, one, h1, C.half(x), hh)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_antisym
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=zero_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=lt_half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift