proposition: Lemma card_partitions_p4 E n m: natp n -> natp m -> cardinal E = n -> cardinal (partitions_pi (variantLc m (n -c m)) E) = binom n m.
proof: Proof. move=> nN mN cE. case: (NleT_el mN nN) => mn. rewrite -(cdiff_pr mn) in cE. by rewrite (card_partitions_p3 mN (NS_diff m nN) cE) (cdiff_pr mn). rewrite binom_bad // (cdiff_wrong (proj1 mn)). have cE': cardinal E = n +c \0c by rewrite csum0r; fprops. set w := partitions_pi _ E; case: (emptyset_dichot w). move=> ->; apply: cardinal_set0. move=> [t] /partitions_piP pip. have [df cVg [fgf duj ue]] := pip. have aux:= (pip_prop0 pip). have ad: inc C0 (domain (variantLc m \0c)) by aww. move: (cVg _ ad); aw=> eq1. have tA:inc C0 (domain t) by rewrite df; aww. by move: (sub_smaller (aux _ tA)); rewrite eq1 cE => /(cltNge mn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)