def natural

stelliferous@0.0.2.0 · proofs/binary_division.bend:150

import Base

150def natural(+n: Nat,+w: Word(n),+b: Nat,+positive: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.divmod(Word.to_nat(n,w),b) == pair(go(n,w,
151      b)) : Nat & Nat}:
152  finish(Word.to_nat(n,w),b,go(n,w,b),go_total(n,w,b),positive,go_bound(n,w,b,positive))