Bytes.to_be_v: 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 298-301 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=298&end_line=301

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
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

def to_be_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +h: {FS.limbs16(one, 16n, xs) == True{} : Bool}) -> {B.to_be(xs) == CV.i2osp(32n, LV.ev(xs)) : List<&2, U32>}:
  %Equal.sym(List<&2, U32>, CV.i2osp(32n, LV.ev(xs)), CV.i2osp_go(32n, LV.ev(xs)), i2_is(32n, LV.ev(xs))) : {B.to_be(xs) == _ : List<&2, U32>}
  %Equal.sym(List<&2, U32>, B.bytes_le(xs), CV.i2osp_le(Nat.double(16n), LV.ev(xs)), bytes_le_v(one, h1, 16n, xs, h)) : {List.reverse(&2, U32, _) == List.reverse(&2, U32, CV.i2osp_le(32n, LV.ev(xs))) : List<&2, U32>}
  {==}

Uses (16):
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=bytes_le_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=i2_is
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=i2osp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=i2osp_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=i2osp_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=limbs16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=bytes_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=to_be