proposition: Lemma card_partitions1 p E: finite_int_fam p -> csum p = cardinal E -> nonempty (partitions_pi p E).
proof: Proof. move=> fif. move /card_eqP => [f [[injf [ff sjf]]] sf tg]. pose k i := (Vg p i) *s1 i. have sx: forall i, inc i (domain p) -> sub (k i) (source f). move=> i idp t tk; rewrite sf; apply /setUb_P1; ex_tac. exists (Lg (domain p) (fun i => Vfs f (k i))); apply /partitions_piP. split; first by aw. move=> i idp; rewrite /k LgV//. rewrite -{2} (card_card (fif_cardinal fif idp)). by rewrite (cardinal_image (sx _ idp) injf) cardinal_indexed. split; first fprops. apply: mutually_disjoint_prop; aw. move=> i j y idp jdp; rewrite !LgV//. move: (sx _ idp)(sx _ jdp)=> p1 p2. move => /(Vf_image_P ff (sx _ idp)) [u uki Wu]. move => /(Vf_image_P ff (sx _ jdp)) [v vkj Wv]. rewrite Wv in Wu. have uv:=(proj2 injf _ _ (p2 _ vkj) (p1 _ uki) Wu). move: uki vkj; rewrite uv /k. by move /indexed_P => [_ _ <-] /indexed_P [_ _ <-]. rewrite -tg;set_extens x. move /setUb_P; aw; move=> [y yd]; move: (sx _ yd) => aux; rewrite LgV//. move=> /(Vf_image_P ff aux) [u uk ->]; Wtac. move=> xtf; move: (sjf _ xtf)=> [y ysf Wy]. move: ysf; rewrite sf; move /disjointU_P=> [pa pb pc]. apply /setUb_P1;ex_tac; apply /(Vf_image_P ff (sx _ pa)). by exists y => //; apply /indexed_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)