def comb_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/proof.bend:106

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as F

106def comb_zero(+n: Nat, +k: Nat, +h: {Nat.is_lt(n, k) == True{} : Bool}) -> S.Comb.zero(n, k, h):
107  Equal.trans(Nat, M.comb(n, k), S.choose(n, k), 0n, F.comb_ok(n, k), F.choose_eq_zero(n, k, h))