def Comb.pascal

bend-collections-laws-crypto@1.0.0.0 · spec/math/natural.bend:194

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

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