ProofU32.div_fin_ok: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
Lines 815-821 of lawful-words@0.1.0.0/proof_u32.bend: https://jend.leeeet.dev/read.txt?path=lawful-words@0.1.0.0/proof_u32.bend&start_line=815&end_line=821

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

def div_fin_ok(+x: Nat, +y: Nat, qr: Word(32n) & U32, d: DMOK(32n, x, y, qr)) -> {U32.to_nat(U32.div.fin(qr)) == Nat.div(x, y) : Nat}:
  match qr:
    case (+q, +r):
      match d:
        case (+e1, +e2):
          %e1 : {Word.to_nat(32n, q) == Nat.div(_, y) : Nat}
          Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(Word.to_nat(32n, q), y), U32.to_nat(r)), y), Word.to_nat(32n, q), N.div_mul_add(Word.to_nat(32n, q), y, U32.to_nat(r), e2))

Uses (14):
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=div_mul_add
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=DMOK