def m256
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/limbs.bend:35
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as Limbs
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/math/typed/width.bend as WW
35def m256(+y: Nat) -> {Nat.mul(y, 256n) == C.shift(8n, y) : Nat}:
36 %Equal.sym(Nat, C.shift(8n, y), Nat.mul(y, C.shift(8n, 1n)), WW.shift_mul(8n, y)) : {Nat.mul(y, 256n) == _ : Nat}
37 {==}