def factorials

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

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

102def factorials(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> S.Comb.factorials(n, k, h):
103  %Equal.sym(Nat, M.comb(n, k), S.choose(n, k), F.comb_ok(n, k)) : {Nat.mul(_, Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))) == S.factorial(n) : Nat}
104  F.choose_mul_facts(n, k, h)