proposition: Lemma card_partitions_p3 E m p: natp m -> natp p -> cardinal E = m +c p -> cardinal (partitions_pi (variantLc m p) E) = binom (m +c p) m.
proof: Proof. move=> mN pN cE; move: (card_partitions_p2 mN pN cE); simpl. set x:= cardinal _. set n := factorial _. set d := (factorial _) *c _. move=> [p1 p2 p3 p4 p5]. have r1: m <=c (m +c p) by apply: csum_M0le; fprops. have r2:((m +c p) -c m = p) by rewrite csumC; apply: cdiff_pr1; fprops. rewrite cprodC in p2. by rewrite (cdivides_pr2 p3 p4 p1 p5 p2) (binom_pr1 (NS_sum mN pN) mN r1) r2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)