NatDivision.small: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_division.bend as NatDivision
Lines 37-44 of stelliferous@0.0.2.0/proofs/nat_division.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&start_line=37&end_line=44

import Base
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

def small(+r: Nat,+b: Nat,h: {Nat.is_lt(r,b) == True{} : Bool}) -> {Nat.divmod(r,b) == (0n,r) : Nat & Nat}:
  match b:
    case 0n:
      Empty.absurd({Nat.divmod(r,0n) == (0n,r) : Nat & Nat},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(r,0n),True{},
            Equal.sym(Bool,Nat.is_lt(r,0n),False{},lt_zero(r)),h)))
    case 1n+ +p:
      %Addition.zero_right(r) : {Nat.divmod.go(r,p,0n,0n) == (0n,_) : Nat & Nat}
      go_small(r,p,0n,0n,lt_succ_le(r,p,h))

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=Empty.absurd
  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.divmod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod.go
  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=Sigma
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&name=go_small
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&name=lt_succ_le
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_division.bend&name=lt_zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=zero_right
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=false_true