proposition: Lemma card_p_subsets n p E: natp n -> natp p -> cardinal E = n -> cardinal (subsets_with_p_elements p E) = binom n p.
proof: Proof. move=> nN pN cEn; symmetry. set src := partitions_pi (variantLc p (n -c p)) E. set trg:= subsets_with_p_elements p E. have cn: cardinalp n by fprops. have cp: cardinalp p by fprops. case: (cleT_el cp cn); last first. move=> np; rewrite binom_bad//. case: (emptyset_dichot trg); first by move=> ->; rewrite cardinal_set0. move=> [y] /Zo_P [] /setP_P yE cy. by move: (sub_smaller yE); rewrite cEn cy =>/(cltNge np). move=> pn. move:(cdiff_pr pn) (NS_diff p nN) => ps sN. move: (cEn); rewrite -ps; move=> cEn'. rewrite -(card_partitions_p3 pN sN cEn') -/src. clear cEn'; apply /card_eqP. exists (Lf (Vg ^~C0) src trg); saw. apply: lf_bijective. - move=> z /partitions_piP pip. have ta: inc C0 (domain z) by move: pip => [p1 _]; rewrite p1; aww. apply: Zo_i; first by move: ((pip_prop0 pip) _ ta) => /setP_P. move: (proj32 pip); aw =>cp'; rewrite (cp' _ inc_C0_C2); aw; trivial. - have aux: forall w, inc w src -> (Vg w C1 = E -s (Vg w C0)). move=> w /partitions_piP [df cVg [fgf duj ue]]. have dgw: (domain w = C2) by rewrite df; aw. rewrite /mutually_disjoint dgw in duj. case: (duj _ _ inc_C0_C2 inc_C1_C2) => di1; first by case:C1_ne_C0. set_extens u; rewrite - ue. move => h1; apply /setC_P; split. union_tac; rewrite dgw; fprops. move=> h2; empty_tac1 u. move /setC_P=> [] /setUb_P [y]; rewrite dgw; case /C2_P => -> //. move=> u v us vs sWa. have sWb: Vg u C1 = Vg v C1 by rewrite (aux _ us) (aux _ vs) sWa. move: us vs => /partitions_piP [df cVg [fgf _ _]] /partitions_piP [df' cV'[fgf' _ _]]. apply: fgraph_exten =>//; first by rewrite df'. by rewrite df; aw;move=> x; case /C2_P => ->. - move=> y /Zo_P [] /setP_P yE cyp. have aux:partition_w_fam (partition_with_complement E y) E. by apply: is_partition_with_complement. exists (variantLc y (E -s y)); aw; trivial. apply /partitions_piP; saw. move=> i itp; try_lvariant itp; trivial. rewrite (cardinal_setC4) ? cEn ? cyp //; apply /NatP; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)