def sh10
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/lits.bend:19
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend as Lits
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
19def sh10(+one: Nat, +h1: {one == 1n : Nat}) -> {C.shift(10n, one) == 1024n : Nat}:
20 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))))))))))