W64mul.dm16: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64mul
Lines 77-81 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend&start_line=77&end_line=81

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

# v(x) == 2^16 hi + (x mod 2^16)
def dm16(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}) -> {Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))) == v(x) : Nat}:
  +e = PD.dm_e(x, c, nz16(c, pc))
  %PD.mul_pow(one, h1, 16n, hi16(x, c), v(c), h16(one, h1, c, pc)) : {Nat.add(_, v(U32.mod(x, c))) == v(x) : Nat}
  e

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend&name=h16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend&name=hi16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend&name=nz16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=dm_e
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&name=mul_pow