U32div.dm_fin: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as U32div
Lines 180-187 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&start_line=180&end_line=187

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

def dm_fin(+aw: Word(32n), +b: U32, qr: Word(32n) & U32, h: inv(32n, aw, v(b), qr)) -> {Nat.add(Nat.mul(v(U32.div.fin(qr)), v(b)), v(U32.mod.fin(qr))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.fin(qr)), v(b)) == True{} : Bool}:
  match qr:
    case (+q, +r):
      (he, hr) = h
      +eq = Equal.trans(Nat, Nat.add(Nat.mul(v(U32{q}), v(b)), v(r)), Nat.add(Nat.mul(S.unsigned(32n, q), v(b)), v(r)), v(U32{aw}),
        Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, v(b)), v(r)), v(U32{q}), S.unsigned(32n, q), vw(q)),
        Equal.trans(Nat, Nat.add(Nat.mul(S.unsigned(32n, q), v(b)), v(r)), S.unsigned(32n, aw), v(U32{aw}), he, Equal.sym(Nat, v(U32{aw}), S.unsigned(32n, aw), vw(aw))))
      (eq, hr)

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.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.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=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.mod.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&name=inv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&name=vw