BinaryDivision.go_bound: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision
Lines 131-136 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=131&end_line=136

import Base

law go_bound:
  for +n: Nat
  for +w: Word(n)
  for +b: Nat
  for positive: {Nat.is_lt(0n,b) == True{} : Bool}
  {Nat.is_lt(remainder(go(n,w,b)),b) == True{} : Bool}

Uses (8):
  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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  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=remainder
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=step_bound