W64est.dsmall: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as W64est
Lines 165-168 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend&start_line=165&end_line=168

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD

# a high word below the divisor: quotient 0, remainder itself
def dsmall(+hi: U32, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}, +bp: Nat, +hb: {v(d) == 1n+bp : Nat}, +hl: {Nat.is_lt(v(hi), 1n+bp) == True{} : Bool}) -> {U32.div(hi, d) == 0 : U32}:
  +e1 = Equal.trans(Nat, v(U32.div(hi, d)), Nat.div(v(hi), v(d)), Nat.div(v(hi), 1n+bp), UD.div_nat(hi, d, hd), Equal.cong(Nat, Nat, z => Nat.div(v(hi), z), v(d), 1n+bp, hb))
  U3.injective(U32.div(hi, d), 0, Equal.trans(Nat, v(U32.div(hi, d)), Nat.div(v(hi), 1n+bp), 0n, e1, NR.div_of(0n, bp, v(hi), hl)))

Uses (13):
  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.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.div
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=injective
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=div_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=div_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend&name=v