BinaryDivision.step_bound: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision
Lines 110-113 of stelliferous@0.0.2.0/proofs/binary_division.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&start_line=110&end_line=113

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

def step_bound(+bit: Bool,+b: Nat,+prev: Quotient,h: {Nat.is_lt(remainder(prev),b) == True{} : Bool}) -> {Nat.is_lt(remainder(step(bit,b,prev)),
    b) == True{} : Bool}:
  Quotient{+q,+r} = prev
  branch_bound(Nat.is_ge(Comparison.digit(bit,r),b),Nat.double(q),Comparison.digit(bit,r),b,{==},Order.digit_lt(r,b,bit,h))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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_ge
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=Quotient
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=branch_bound
  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/binary_division.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=digit_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_comparison.bend&name=digit