proposition: Lemma card_partitions6 p E f h: finite_int_fam p -> csum p = cardinal E -> partition_with_pi_elements p E f -> inc h (permutations E) -> lf_axiom (fun g=> Lg (domain p)(fun i=> (restriction2 ((inverse_fun h) \co g) (Vg f i) (Vg f i)))) (Zo (permutations E) (fun g => (partitions_aux f g = partitions_aux f h))) (productb (Lg (domain p)(fun i=> (permutations (Vg f i))))).
proof: Proof. move=> fip spE pip hp g; move: (pip_prop0 pip)=> Ht. move: (pip) => [df cVg [fgf duj ue]]. move /Zo_P => [gp eql]; apply /setXb_P; fprops;split;aww. move=> i idp; rewrite !LgV//. move: eql; move /(card_partitions5P fip spE pip hp gp) => eql. move: (eql _ idp) => ic; clear eql. move: hp gp => /Zo_P [] /functionsP [fh sh th] bh. move=> /Zo_P [] /functionsP [fg sg tg] bg. have fih: function (inverse_fun h) by apply: bijective_inv_f. have cih: (inverse_fun h) \coP g by saw; ue. have fcih : function ((inverse_fun h) \co g) by fct_tac. set k:= restriction2 _ _ _. have sk: source k = Vg f i by rewrite /k/restriction2; aw. have tk: target k = Vg f i by rewrite /k/restriction2; aw. rewrite df in Ht; move: (Ht _ idp) => Ht1. have ra: (restriction2_axioms (compose (inverse_fun h) g) (Vg f i) (Vg f i)). hnf; saw; ue. have fk: (function k) by rewrite /k; apply: (proj31(restriction2_prop ra)). apply:permutation_if_inj. - rewrite /finite_set;move: pip fip => [_ pip _] [hp _ ]. by rewrite (pip _ idp); apply/NatP; apply: hp. - done. split=>// x y; rewrite sk => xsk ysk. rewrite /k restriction2_V //restriction2_V //. move: (Ht1 _ xsk) (Ht1 _ ysk); rewrite - sg => xsg ysg. rewrite !compfV// ;move => eq. move: bg=> [[_ ig] _ ]; apply: (ig _ _ xsg ysg). move: (inverse_bij_fb bh) => [[_ iih] _ ]. move:iih; aw; apply =>//; try (rewrite th -tg; Wtac). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)