U32Division.divide: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_division.bend as U32Division
Lines 149-159 of stelliferous@0.0.2.0/proofs/u32_division.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&start_line=149&end_line=159

import Base
import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision

def divide(+a: U32,+b: U32,+cap: U32,+cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},+divisor_bound: {Nat.is_le(Nat.double(U32.to_nat(b)),
      U32.to_nat(cap)) == True{} : Bool},+positive: {Nat.is_lt(0n,U32.to_nat(b)) == True{} : Bool}) -> {U32.to_nat(U32.div(a,
      b)) == Nat.div(U32.to_nat(a),U32.to_nat(b)) : Nat}:
  U32{+w} = a
  U32{+bw} = b
  +b = {U32{bw} : U32}
  %Equal.sym(Bool,U32.is_zero(b),False{},nonzero(b,positive)) : {U32.to_nat(U32.div.if(w,b,_)) == Nat.div(Word.to_nat(32n,w),U32.to_nat(b)) : Nat}
  %Equal.sym(Nat,Nat.div(Word.to_nat(32n,w),U32.to_nat(b)),quotient(BinaryDivision.go(32n,w,U32.to_nat(b))),natural_quotient(w,U32.to_nat(b),
      positive)) : {U32.to_nat(U32.div.fin(U32.divmod.go(32n,w,b))) == _ : Nat}
  %go(32n,w,b,cap,cap_ok,divisor_bound,positive) : {U32.to_nat(U32.div.fin(U32.divmod.go(32n,w,b))) == quotient(_) : Nat}
  quotient_decode(U32.divmod.go(32n,w,b))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  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.div.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div.if
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  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.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=go
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=go
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=natural_quotient
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=nonzero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=quotient
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=quotient_decode