~/jendhub

def internal_mod_go_small

bend-mathlib@0.8.1.0 · nat.bend:1988

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

1988def 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}:
1989  match n:
1990    case 0n:
1991      {==}
1992    case 1n++np:
1993      %add_succ(np, r) : {Pair.snd(Nat, Nat, Nat.divmod.go(np, Nat.add(np, k), d, 1n+r)) == _ : Nat}
1994      internal_mod_go_small(np, k, d, 1n+r)

Uses (5)

Used by (1)