def Comb.factorials

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

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

198def Comb.factorials(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> Type:
199  {Nat.mul(M.comb(n, k), Nat.mul(factorial(k), factorial(Nat.sub(n, k)))) == factorial(n) : Nat}