ProofU32.mod_fin_ok: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
Lines 823-829 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=823&end_line=829

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

def mod_fin_ok(+x: Nat, +y: Nat, qr: Word(32n) & U32, d: DMOK(32n, x, y, qr)) -> {U32.to_nat(U32.mod.fin(qr)) == Nat.mod(x, y) : Nat}:
  match qr:
    case (+q, +r):
      match d:
        case (+e1, +e2):
          %e1 : {U32.to_nat(r) == Nat.mod(_, y) : Nat}
          Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Word.to_nat(32n, q), y), U32.to_nat(r)), y), U32.to_nat(r), N.mod_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.mod
  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.mod.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=mod_mul_add
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=DMOK