def mul_v
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:165
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as Limbs
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as PD
165def mul_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +h: {Nat.is_lt(Nat.mul(v(x), v(y)), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.mul(x, y)) == Nat.mul(v(x), v(y)) : Nat}:
166 PD.mul32(one, h1, x, y, h)