U32Division.natural_quotient: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_division.bend as U32Division
Lines 126-130 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=126&end_line=130

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

def natural_quotient(+w: Word(32n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.div(Word.to_nat(32n,w),
    b) == quotient(BinaryDivision.go(32n,w,b)) : Nat}:
  %Equal.sym(Nat & Nat,Nat.divmod(Word.to_nat(32n,w),b),BinaryDivision.pair(BinaryDivision.go(32n,w,b)),BinaryDivision.natural(32n,w,b,
      positive)) : {Pair.fst(Nat,Nat,_) == quotient(BinaryDivision.go(32n,w,b)) : Nat}
  quotient_pair(BinaryDivision.go(32n,w,b))

Uses (15):
  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.divmod
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  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=stelliferous@0.0.2.0/proofs/binary_division.bend&name=go
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=natural
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=pair
  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_pair