Word.mul_exact: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as Word
Lines 63-67 of bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&start_line=63&end_line=67

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as WM
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as NM

# multiplication below 2^n is exact
def mul_exact(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +a: Word(n), +b: Word(n), +h: {Nat.is_lt(Nat.mul(uw(n, a), uw(n, b)), sc(n, one)) == True{} : Bool}) -> {uw(n, Word.mul(n, a, b)) == Nat.mul(uw(n, a), uw(n, b)) : Nat}:
  +p = Nat.mul(uw(n, a), uw(n, b))
  %Equal.sym(Word(n), Word.mul(n, a, b), S.from_nat(n, p), WM.refines(n, a, b)) : {S.unsigned(n, _) == p : Nat}
  WV.from_nat_value(n, p, L.subst(Nat, z => {Nat.is_lt(p, z) == True{} : Bool}, S.scale_binary(n, 1n), Nat.pow(2n, n), NM.scale_power(n), lt1(n, one, h1, p, h)))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend&name=scale_power
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend&name=refines
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend&name=from_nat_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=scale_binary
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=lt1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=uw