proposition: Lemma card_partitions_p2 E m p (num := factorial (m +c p)) (den := (factorial m) *c (factorial p)) (x := cardinal (partitions_pi (variantLc m p) E)): natp m -> natp p -> cardinal E = (m +c p) -> [/\ natp x, num = x *c den,natp num, natp den & den <> \0c].
proof: Proof. move=> mN pN cE. set P:= variantLc m p. have h1: finite_int_fam P. rewrite /P;split;fprops. by hnf; aw; move=> i it; try_lvariant it. aw;apply: set2_finite. have p2: csum P = cardinal E. symmetry;rewrite cE /csum2/csum; fprops. move: (card_partitions h1 p2); simpl. set y:= cprodb _ _. have -> : den = y. rewrite /den/cprod2/y/P; aw; apply:cprodb_exten. move=> xx xtp /=; try_lvariant xtp; fprops. rewrite cE; move=> [r1 r2 r3 r4 r5];split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)