law go_total

stelliferous@0.0.2.0 · proofs/binary_division.bend:115

import Base

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