~/jendhub

def div_rest

bendtorch@1.3.0.0 · PROOF.bend:854

import bendtorch@1.3.0.0/PROOF.bend as PROOF
import Base

854# fewer than 1 + s numbers after the last whole block leave the quotient alone
855def div_rest(+i: Nat, -k: Nat, -d: Nat, -r: Nat) -> {Pair.fst(Nat, Nat, Nat.divmod.go(i, Nat.add(i, k), d, r)) == d : Nat}:
856  match i:
857    case 0n:
858      {==}
859    case 1n+p:
860      div_rest(p, k, d, 1n+r)

Uses (4)

Used by (1)