def internal_div_go_small

bend-mathlib@0.8.1.0 · nat.bend:800

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

import Base

800def internal_div_go_small(n: Nat, +k: Nat, +d: Nat, r: Nat) -> {d == Pair.fst(Nat, Nat, Nat.divmod.go(n, Nat.add(n, k), d, r)) : Nat}:
801  match n:
802    case 0n:
803      {==}
804    case 1n+np:
805      internal_div_go_small(np, k, d, 1n+r)

Uses (4)

Used by (2)