proposition: Theorem card_partitions p E (num:= factorial (cardinal E)) (den := cprodb (domain p) (fun z => factorial (Vg p z))): finite_int_fam p -> csum p = cardinal E -> [/\ num = cardinal (partitions_pi p E) *c den, natp num, natp den, den <> \0c & finite_set (partitions_pi p E)].
proof: Proof. move => fip spe. move: (card_partitions1 fip spe)=> [h hp]. have Hb: finite_set E. by hnf; rewrite - spe; apply /NatP; apply: finite_sum_finite=> //. have numN: natp num by rewrite /num; apply: NS_factorial; apply /NatP; aw. have ndenN: natp den. move: fip=> [p2 p3]. rewrite /den;apply: finite_product_finite =>//. by hnf; saw; hnf; aw => i idp; rewrite LgV//; apply: NS_factorial; apply: p2. have nd:den <> \0c. move: fip=> [p2 p3]. apply /cprod_nzP; hnf;aw => i idp; rewrite LgV//; apply: factorial_nz; apply: p2=>//. rewrite /finite_set; set aux:= cardinal _. suff: num = aux *c den. move => eql; split => //. by apply /NatP /(NS_in_product (CS_cardinal (partitions_pi p E)) nd);ue. move: hp => /Zo_P [hfpp pip]. move:(card_partitions4 fip spe pip). set phi:= Lf _ _ _; move=> sjphi. suff phip: forall x, inc x (target phi) -> cardinal (Vfi1 phi x) = den. move: sjphi=> [fphi _]. move:(shepherd_principle fphi phip). rewrite /phi lf_source lf_target card_permutations //. move=> x xt. move:((proj2 sjphi) _ xt) => [y ys yw]. move: ys; rewrite {1}/ phi; aw => yp. move: (card_bijection (card_partitions7 fip spe pip yp)). rewrite lf_source lf_target; congr (cardinal _ = _); last first. apply: Eqc_setXb; split;aww => i idp; rewrite !LgV//. move: pip (proj1 fip _ idp)=>[p1 p2 [p3 _ _]] /NatP fv. rewrite card_permutations /finite_set (p2 _ idp) // card_card //. by apply:CS_factorial. have Ha:lf_axiom (fun g => (partitions_aux h g)) (permutations E) (partitions_pi p E). by move => g gp; apply: card_partitions3. have fphi: function phi by fct_tac. set_extens t. move /Zo_P => [pa pb]. apply: (iim_fun_set1_i fphi); rewrite /phi; aw; trivial. by rewrite yw /phi ! LfV. case /(iim_fun_set1_P _ fphi); rewrite /phi lf_source => ta. by rewrite LfV// => tb; apply: Zo_i => //; rewrite - tb yw /phi LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)