proposition: Theorem card_partitions_bis p E: finite_int_fam p -> csum p = cardinal E -> cardinal (partitions_pi p E) = (factorial (cardinal E)) %/c (cprodb (domain p) (fun z => factorial (Vg p z))).
proof: Proof. move=> h1 h2. move: (card_partitions h1 h2) => [p1 p2 p3 p4] /NatP p5. by rewrite p1 cprodC; symmetry; apply: cdivides_pr4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)