law go_bound

stelliferous@0.0.2.0 · proofs/binary_division.bend:131

import Base

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