PROOF.um.e: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 1449-1450 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=1449&end_line=1450

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws

def um.e(+n: Nat, +a: Word(n), +b: Word(n)) -> {Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, um.k(n, n, a, b, Word.zero(n)))) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}:
  Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, um.k(n, n, a, b, Word.zero(n)))), Nat.add(0n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, um.k(n, n, a, b, Word.zero(n)))), Nat.add(Word.to_nat(n, Word.zero(n)), Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), Nat.add(0n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), um.go(n, n, a, b, Word.zero(n)), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), Word.to_nat(n, Word.zero(n)), 0n, Laws.word_zero_value(n))), {==})

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Nat.mul
  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=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_zero_value
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=um.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=um.k
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl