Natural.comb_go: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as Natural
Lines 136-143 of bend-collections-laws-math@1.0.0.0/src/math/natural.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&start_line=136&end_line=143

import Base

# r_{i+1} = r_i * (n - i) / (i + 1): every r_i is C(n, i), so the division
# is exact (reference section 8.6).
def comb_go(j: Nat, +n: Nat, +i: Nat, +r: Nat) -> Nat:
  match j:
    case 0n:
      r
    case 1n+ +jp:
      comb_go(jp, n, 1n+i, Nat.div(Nat.mul(r, Nat.sub(n, i)), 1n+i))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub