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

import Base

law go_total:
  for +n: Nat
  for +w: Word(n)
  for +b: Nat
  {total(go(n,w,b),b) == Word.to_nat(n,w) : Nat}

Uses (11):
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  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_digit.bend&name=word_digit
  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=step
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=step_total
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/binary_division.bend&name=total
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_comparison.bend&name=digit