proposition: Lemma card_partitions4 p E f: finite_int_fam p -> csum p = cardinal E -> partition_with_pi_elements p E f -> surjection (Lf (partitions_aux f) (permutations E) (partitions_pi p E)).
proof: Proof. move=> fip spE [df cVg pfa];move:(pfa)=> [fgf duj ue]. set phi:=Lf _ _ _. apply: lf_surjective; first by move=> g; apply: card_partitions3. have Ha:finite_set E by hnf;rewrite - spE; apply /NatP /finite_sum_finite. move=> y /partitions_piP [dy cVy [fgy dujy uey]]. pose ha i := equipotent_ex (Vg f i) (Vg y i). have hap: forall i, inc i (domain p) -> bijection_prop (ha i) (Vg f i) (Vg y i). move=> i idp; apply: equipotent_ex_pr. by apply /card_eqP; rewrite (cVg _ idp) (cVy _ idp). pose h i := Lf (Vf (ha i)) (Vg f i) E. have ta1:forall i, inc i (domain p) -> lf_axiom (Vf (ha i)) (Vg f i) E. move=> i idp z zW. move: (hap _ idp)=> [[[fh _] _] sh th]. rewrite - sh in zW;move: (Vf_target fh zW); rewrite th -uey. move=> h1; apply /setUb_P; exists i => //; ue. have fp1:(forall i, inc i (domain f) -> function_prop (h i) (Vg f i) E). rewrite df /h=> i idp; saw; apply: lf_function; apply: ta1 =>//. rewrite -df in hap. move: (extension_partition1 pfa fp1). set g := common_ext _ _ _; move=> [[fg sg tg] extg]. have injg: injection g. split=> //; move=> u v. rewrite sg -ue; move=> /setUb_P [u' u'd Vu'] /setUb_P [v' v'd Vv']. have pu : Vf g u = Vf (ha u') u. move: (extg _ u'd) => [p1 p2 ->] //;rewrite /h LfV//; apply: ta1; ue. have pv: Vf g v = Vf (ha v') v. move: (extg _ v'd)=> [p1 p2 -> ] //; rewrite /h LfV//; apply: ta1; ue. move=> eq; suff:u' = v'. move: (hap _ u'd) => [[[_ ih] _] sa _] aux. by rewrite sa in ih; apply: ih =>//; rewrite - ? pu ? aux // eq pv. case: (duj _ _ u'd v'd) =>// dj. have Wu: (inc (Vf g u) (Vg y u')). rewrite pu; move: (hap _ u'd) => [[fh _] sa <-]; Wtac; fct_tac. have Wv: (inc (Vf g v) (Vg y v')). rewrite pv; move: (hap _ v'd) => [[fh _] sa <-]; Wtac; fct_tac. hnf in dujy; rewrite dy -df in dujy. case: (dujy _ _ u'd v'd) =>// h1; rewrite eq in Wu; empty_tac1 (Vf g v). have pg: inc g (permutations E) by apply: permutation_if_inj. ex_tac; symmetry. rewrite /partitions_aux; apply: fgraph_exten =>//; [ fprops | aw; ue|]. aw; move=> x xdf /=; rewrite LgV//. move: (hap _ xdf) => [bha sha tha]. move: (fp1 _ xdf) (extg _ xdf) => [fh sh th] [p2a _ p2c]. have p3 : forall i, inc i (Vg f x) -> Vf g i = Vf (ha x) i. move=> i ins; rewrite (p2c _ ins) /h LfV//; apply: ta1 =>//; ue. rewrite -tha. set_extens u. move /(Vf_image_P fg p2a)=> [i ins ->]; rewrite (p3 _ ins); Wtac;fct_tac. move: bha => [iha sjha] ut. move: (proj2 sjha _ ut)=> [v vs ->]. rewrite sha in vs; rewrite - (p3 _ vs); apply /(Vf_image_P fg p2a); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)