proposition: Lemma card_partitions7 p E f h: finite_int_fam p -> csum p = cardinal E -> partition_with_pi_elements p E f -> inc h (permutations E) -> bijection (Lf (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; move: (pip_prop0 pip)=> sWE. move: (pip) => [df cVg [fgf duj ue]]; move: (proj33 pip) => pfa. rewrite df in sWE. set ww:=Lf _ _ _. move: (card_partitions6 fip spE pip hp) => ta. move:(hp) => /Zo_P [] /functionsP [fh sh th] bh. have bih: (bijection (inverse_fun h)) by apply: inverse_bij_fb. have fw: function ww by apply: lf_function. have sw: surjection ww. split => // y. rewrite {1 2} /ww; aw; move /setXb_P; aw; move=> [fgy dy yp]. have yp': (forall i, inc i (domain p) -> (bijection_prop (Vg y i) (Vg f i) (Vg f i))). by move=> i idp;move: (yp _ idp); rewrite LgV//;move => /Zo_P [/functionsP [? ? ?] ?]. have ta1: (forall i, inc i (domain p) -> lf_axiom (Vf (Vg y i)) (Vg f i) E). move=> i idp z zW; move: (yp' _ idp)=> [bha sha tha]. apply: (sWE _ idp); rewrite -tha;Wtac; fct_tac. pose hb i := Lf (Vf (Vg y i)) (Vg f i) E. have Hw:forall i, inc i (domain f) -> function_prop (hb i) (Vg f i) E. rewrite df; move => i ip; rewrite /hb /function_prop lf_source lf_target. split => //; apply: lf_function;apply: ta1 =>//. move: (extension_partition1 pfa Hw). set g := common_ext _ _ _; move => [[fg sg tg] alag]. have ijg: injection g. split=>// u v; rewrite sg => uE vE. move: uE vE;rewrite -ue; move=> /setUb_P [a adf ua] /setUb_P [b bdf vb]. move: (alag _ adf)(alag _ bdf) => [p1 p2 p3] [q1 q2 q3]. have ap: inc a (domain p) by ue. have bp: inc b (domain p) by ue. move : (ta1 _ ap) (ta1 _ bp) => ta2 ta3. rewrite (p3 _ ua)(q3 _ vb) /hb (LfV ta2 ua) (LfV ta3 vb). move: (yp' _ ap) (yp' _ bp)=> [[[_ iha] xx] sha tha] [yy shb thb]. case: (duj _ _ adf bdf). move=> ab; rewrite -ab in vb; rewrite -ab. apply: iha; rewrite sha //. move=> h1 h2; empty_tac1 (Vf (Vg y a) u). - rewrite /Vf in tha;rewrite -tha; Wtac; fct_tac. - rewrite /Vf in thb;rewrite h2 -thb; Wtac; fct_tac. have gp: inc g (permutations E). apply:permutation_if_inj => //. apply /NatP; rewrite - spE; apply: finite_sum_finite =>//. move/permutationsP:(gp) => [bg _ _]. have pa:forall i v, inc i(domain p) -> inc v (Vg f i) -> Vf g v = Vf (Vg y i) v. rewrite -df;move=> i v idp; move: (alag _ idp). rewrite /agrees_on; move => [s1 s2 aux]. move=> vW;move:(aux _ vW); rewrite /hb LfV; [done | apply: ta1;ue| done ]. have pb:forall i v, inc i (domain p)-> inc v (Vg f i) -> inc (Vf g v)(Vg f i). move=> i v ip iv; rewrite (pa _ _ ip iv). move: (yp' _ ip) => [bha sha tha]; Wtac; fct_tac. set (t:= h \co g). have pt: inc t (permutations E) by apply (permutation_Sc hp gp). set z:=Zo _ _. have xz:inc t z. apply: Zo_i => //. rewrite /partitions_aux df; apply: Lg_exten. move=> i idp /=; set_extens u; aw. move /dirim_P => [a ai]; rewrite /t /compose; aw. move /compg_pP => [b Jg1 Jg2]; apply /dirim_P; ex_tac. by move: (Vf_pr fg Jg1) => ->; apply: pb. move=> /dirim_P [a asVf Jg]. have atg: inc a (target g) by rewrite tg; apply: (sWE _ idp). move: (bg) => [_ sjg]; move: ((proj2 sjg) _ atg) => [b bsg Wb]. move: (bsg); rewrite sg; rewrite -ue; move /setUb_P => [j jd aw]. apply /dirim_P. rewrite -df in idp pb; case: (duj _ _ idp jd) => di. rewrite -di in aw; ex_tac. rewrite /t /compose; aw; apply /compg_pP; ex_tac; rewrite Wb; Wtac. empty_tac1 a; rewrite Wb;apply: (pb _ _ jd aw). ex_tac; rewrite (LfV ta xz). rewrite /t (permutation_lK hp gp). symmetry;apply: fgraph_exten;aw; fprops => x xdp; aw. move: (sWE _ xdp)=> Wf. have ra: (restriction2_axioms g (Vg f x) (Vg f x)). have ssg: sub (Vg f x) (source g) by rewrite sg. have stg: sub (Vg f x) (target g) by rewrite tg. split => //; move=> u /(Vf_image_P fg ssg) [v vW ->]; apply: (pb _ _ xdp vW). move : (yp' _ xdp) => [bha sha tha]. rewrite LgV//; apply: function_exten. - by apply: (proj31 (restriction2_prop ra)). - fct_tac. - by rewrite /restriction2 sha corresp_s. - by rewrite /restriction2 tha corresp_t. - rewrite /restriction2; aw; move=> u uW /=; rewrite restriction2_V //. by rewrite (pa _ _ xdp uW). split=>//; split =>//. rewrite /ww lf_source=> x y xS yS; rewrite (LfV ta xS) (LfV ta yS). move: xS yS => /Zo_P [xs eq1] /Zo_P [ys eq2]. move: eq1 => /(card_partitions5P fip spE pip hp xs). move: eq2 => /(card_partitions5P fip spE pip hp ys). set xi:= _ \co x; set yi:= _ \co y => eq2 eq1 eq. suff: xi = yi. rewrite /xi /yi;move => eqi; move: (f_equal (compose h) eqi). by rewrite (permutation_lK' hp xs)(permutation_lK' hp ys). move:(permutation_Si hp) => hp'. move:(permutation_Sc hp' xs) => /permutationsP[ /proj1/proj1 bxi sxi txi]. move:(permutation_Sc hp' ys) => /permutationsP[ /proj1/proj1 byi syi tyi]. apply: (function_exten bxi byi). by rewrite sxi syi. by rewrite txi tyi. rewrite sxi -ue;move=> u; move /setUb_P; rewrite df; move=> [i ip iW]. move: (f_equal (Vg ^~i) eq); rewrite !LgV// => eq3. have ra:restriction2_axioms xi (Vg f i) (Vg f i). split => //; last (by rewrite eq1; fprops); rewrite ?sxi ?txi;apply: (sWE _ ip). have rb:restriction2_axioms yi (Vg f i) (Vg f i). split => //; last (by rewrite eq2; fprops); rewrite ? syi ? tyi; apply: (sWE _ ip). move: (f_equal (Vf ^~u) eq3);rewrite restriction2_V // restriction2_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)