Lits.sh10: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend as Lits
Lines 19-20 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend&start_line=19&end_line=20

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

def sh10(+one: Nat, +h1: {one == 1n : Nat}) -> {C.shift(10n, one) == 1024n : Nat}:
  shk(9n, one, 512n, shk(8n, one, 256n, shk(7n, one, 128n, shk(6n, one, 64n, shk(5n, one, 32n, shk(4n, one, 16n, shk(3n, one, 8n, shk(2n, one, 4n, shk(1n, one, 2n, shk(0n, one, 1n, h1))))))))))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend&name=shk
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift