def Comb.zero

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

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

201# PDF 8.6: comb(n, k) is 0 for k > n, not an error
202def Comb.zero(+n: Nat, +k: Nat, +h: {Nat.is_lt(n, k) == True{} : Bool}) -> Type:
203  {M.comb(n, k) == 0n : Nat}