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

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

def natural_remainder(+w: Word(32n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.mod(Word.to_nat(32n,w),
    b) == BinaryDivision.remainder(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.snd(Nat,Nat,_) == BinaryDivision.remainder(BinaryDivision.go(32n,w,b)) : Nat}
  remainder_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.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=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  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/binary_division.bend&name=remainder
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_division.bend&name=remainder_pair