Nat.internal_mod_go_small: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/nat.bend as Nat
Lines 1988-1994 of bend-mathlib@0.8.1.0/nat.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/nat.bend&start_line=1988&end_line=1994

import Base

def internal_mod_go_small(n: Nat, -k: Nat, -d: Nat, +r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, Nat.add(n, k), d, r)) == Nat.add(n, r) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n++np:
      %add_succ(np, r) : {Pair.snd(Nat, Nat, Nat.divmod.go(np, Nat.add(np, k), d, 1n+r)) == _ : Nat}
      internal_mod_go_small(np, k, d, 1n+r)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_succ