proposition: Lemma partition_nq_pr5c E: finite_set E -> cardinal (partition_nq E \1c) = Ex59_val \1c (cardinal E).
proof: Proof. move => /NatP nN; rewrite /Ex59_val/Ex59_num/Ex59_den. have fN:=(NS_factorial nN). rewrite partition_nq_pr5b factorial1 cpow1x (cprod1l (CS_nat nN)). by rewrite (cprod1r (CS_nat fN)) (cquo_itself fN (factorial_nz nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)