def acc2

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:494

import Base

494def acc2(i: Nat, m: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(i, m, 1n+d, r) == bump2(Nat.divmod.go(i, m, d, r)) : Nat & Nat}:
495  match i m:
496    case 0n _:
497      {==}
498    case 1n+np 0n:
499      acc2(np, r, 1n+d, 0n)
500    case 1n+np 1n+mp:
501      acc2(np, mp, d, 1n+r)