Natural.Comb.pascal: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as Natural
Lines 194-196 of bend-collections-laws-math@1.0.0.0/spec/math/natural.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/natural.bend&start_line=194&end_line=196

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

# Pascal's rule on the implementation itself
def Comb.pascal(+m: Nat, +j: Nat) -> Type:
  {M.comb(1n+m, 1n+j) == Nat.add(M.comb(m, j), M.comb(m, 1n+j)) : Nat}

Uses (3):
  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=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=comb