proposition: Lemma partition_nq_pr9 E q n: natp n -> natp q -> \0c <c q -> cardinal E = q *c n -> cardinal (partition_nq E q) *c (Ex59_den q n) = (Ex59_num q n) .
proof: Proof. move => nN qN qp cardE. move:(partition_nq_pr7 qp cardE) => [p0 p0p]. move /Zo_P: (p0p) => [/Zo_P [/setP_P ha [[hb hc] hd]] he]. pose F f:= extension_p3 f p0. have Ha: forall f, inc f (permutations E) -> inc (F f) (partition_nq E q). by move => f/permutationsP fp; apply: (partition_nq_pr6c fp p0p). set F0 := Lf F (permutations E) (partition_nq E q). have fF0: function F0 by apply: lf_function. have <-: cardinal (source F0) = Ex59_num q n. rewrite /F0 lf_source (card_permutations) ?cardE //. apply/NatP; rewrite cardE; fprops. suff kk: forall x, inc x (target F0) -> cardinal (Vfi1 F0 x) = Ex59_den q n. by rewrite (shepherd_principle fF0 kk) lf_target. rewrite lf_target => x xp. have px:inc p0 (\Po (\Po E)) by apply /setP_P. rewrite (iim_fun_set1_E _ fF0) lf_source. move: (partition_nq_pr8 qN (nesym (proj2 qp)) p0p xp) => [sig sigp <-]. set T := Zo _ _. have ->: T = Zo (permutations E) (fun f => F ((inverse_fun sig) \co f) = p0). apply: Zo_exten1 => t tE;rewrite /F0 LfV//. move/permutationsP: tE => pa. move/permutationsP: sigp => pb; move :(inverse_bij_bp pb) => pc. rewrite /F - (ext2_pr6 pa pc px); split => sa. by rewrite - sa (ext2_pr7 pb px). rewrite - (ext2_pr7 pc (ext2_pr5 pa px)). rewrite -{1} sa - {1} (ifun_involutive (proj1 (proj1 (proj31 pb)))) //. transitivity (cardinal (Zo (permutations E) (fun f => F f = p0))). apply/card_eqP; set A := Zo _ _; set B := Zo _ _. exists (Lf (fun f => (inverse_fun sig \co f)) A B);saw. apply:lf_bijective. - move => f /Zo_P[pa pb]; apply/Zo_P; split => //. apply: (permutation_Sc (permutation_Si sigp) pa). - move => u v /Zo_S up /Zo_S vp => /(f_equal (compose sig)). by rewrite (permutation_lK' sigp up) (permutation_lK' sigp vp). - move => y /Zo_P[pa pb]; move:(permutation_lK sigp pa) => pc. exists (sig \co y) => //; apply/Zo_P; rewrite pc; split=> //. apply:(permutation_Sc sigp pa). clear sigp T x xp. set In := Nint n; set Iq := Nint q. have: cardinal p0 = n. apply:(partition_nq_pr2 (CS_nat nN) qN (nesym (proj2 qp)) cardE p0p). rewrite -{1} (card_Nint nN) -/In => /card_eqP [fa [bfa sfa tfa]]. have bifa: bijection_prop (inverse_fun fa) In p0. hnf;aw; split => //;exact:(inverse_bij_fb bfa). have fifa := proj1 (proj1 (proj31 bifa)). pose fb:= graph (inverse_fun fa). have dfb: domain fb = In. move:bifa => [/proj1/proj1 ra <- _]; exact: (domain_fg ra). have rfb: forall i, inc i In -> inc (Vf (inverse_fun fa) i) p0. move:bifa => [ra rb rc] i iN; Wtac. have rfb': forall i, inc i In -> inc (Vg fb i) p0 by []. have injfb i j: inc i In -> inc j In -> (Vg fb i) = (Vg fb j) -> i = j. by move => ii ji /(f_equal (Vf fa)); rewrite !(inverse_V bfa) // tfa. have pfa1 : forall i, inc i In -> sub (Vg fb i) E. by move => i iN; apply /setP_P /ha /(rfb' _ iN). have pfa:partition_w_fam fb E. move:bifa => [ra rb rc]; split. - exact: (proj32 fifa). - apply:(mutually_disjoint_prop1 fifa); rewrite rb => i j y ii ji sa sb. case:(hc _ _ (rfb _ ii) (rfb _ ji)) => //; last by move => di; empty_tac1 y. apply:(injfb _ _ ii ji). - set_extens t; first by move/setUb_P => [y ya yb]; apply: pfa1 yb; ue. rewrite - hb;move/setU_P => [y ya yb]; apply/setUb_P; exists (Vf fa y). rewrite dfb - tfa; Wtac; fct_tac. by rewrite -/(Vf _ _) inverse_V2 // sfa. have pfa2:forall x,singl_val2 (inc^~ In) (fun z=> inc x (Vg fb z)). move:(pfa) => [ra rb rc] x; rewrite -dfb /= => i j ii rd jj re. case: (rb _ _ ii jj) => // di; empty_tac1 x. pose fc x:= select (fun z => inc x (Vg fb z)) In. have pfa3: forall x, inc x E -> inc x (Vg fb (fc x)) /\ inc (fc x) In. move:(pfa) => [ra rb rc]. move => x xE; apply:(select_pr) (pfa2 x). by move:xE; rewrite - rc - dfb => /setUb_P. pose fi i:= equipotent_ex (Vg fb i) Iq. have fibig: forall i, inc i In -> bijection_prop (fi i) (Vg fb i) Iq. move => i id; apply /equipotent_ex_pr/card_eqP. move:bifa => [ra rb rc]. by rewrite (card_Nint qN) -/(Vf _ _); apply: he; Wtac; rewrite rb - dfb. set sPhi:= permutations In \times (gfunctions In (permutations Iq)). have ->: Ex59_den q n = cardinal sPhi. have ra:=(card_Nint nN). have rb: finite_set In by apply/NatP; rewrite ra. have ra':=(card_Nint qN). have rb': finite_set Iq by apply/NatP; rewrite ra'. rewrite - cprod2_pr1 - cprod2cl - cprod2cr (card_permutations rb) ra. move /card_eqP: (Eq_fun_set In (permutations Iq)) => <-. by rewrite cpow_pr1 ra (card_permutations rb') ra'. have sphi_p1: forall x, inc x sPhi -> [/\ pairp x, inc (P x) (permutations In) & forall i, inc i In -> inc (Vg (Q x) i) (permutations Iq)]. move => x /setX_P [ra rb /gfunctions_P2 [rc1 rc2 rc3]]; split => //. by move => i ii; apply: rc3; apply: (inc_V_range rc1); rewrite rc2. pose h1 x i t := (Vf (inverse_fun (fi (Vf (P x) i))) (Vf (Vg (Q x) i) (Vf (fi i) t))). have h1p: forall x i t, inc x sPhi -> inc i In -> inc t (Vg fb i) -> inc (h1 x i t) (Vg fb (Vf (P x) i)) /\ inc (h1 x i t) E. move => x i t /sphi_p1 [_ /permutationsP ra rb] ii th; rewrite /h1. move:(fibig _ ii) => [/proj1/proj1 sa sb sc]. have: inc (Vf (fi i) t) Iq by Wtac. set y := (Vf (fi i) t) => sd. move: (rb _ ii) => /permutationsP [wa1 wa2 wa3]. set z := (Vf (Vg (Q x) i) y). have zp: inc z Iq by rewrite/z; Wtac; fct_tac. have ji: inc (Vf (P x) i) In by move: ra => [[[ra1 _] _] ra2 <-]; Wtac. move: (inverse_bij_bp (fibig _ ji)) => [se sf sg]; set a := Vf _ _. have aej: inc a (Vg fb (Vf (P x) i)) by rewrite /a; Wtac; fct_tac. split => //;exact:(pfa1 _ ji _ aej). have h1p': forall x i, inc x sPhi -> inc i In -> lf_axiom (h1 x i) (Vg fb i) E. move => x i ra rb t tx; exact: (proj2 (h1p _ _ t ra rb tx)). pose h2 x i := Lf (h1 x i) (Vg fb i) E. have h2a: forall x i, inc x sPhi -> inc i In -> function_prop (h2 x i) (Vg fb i) E. rewrite /h2 => x i ra rb;saw;apply: (lf_function (h1p' _ _ ra rb)). pose h3 x := common_ext fb (h2 x) E. have h3p1: forall x, inc x sPhi -> function_prop (h3 x) E E /\ (forall i, inc i (domain fb) -> agrees_on (Vg fb i) (h3 x) (h2 x i)). move => x xs; apply: (extension_partition1 pfa) => i; rewrite dfb //; fprops. have h3p2: forall x i t, inc x sPhi -> inc i (Nint n) -> inc t (Vg fb i) -> Vf (h3 x) t = h1 x i t /\ inc (Vf (h3 x) t) (Vg fb (Vf (P x) i)). move => x i t ra rb rc; move: (proj1 (h1p _ _ t ra rb rc)). move: (proj2 (h3p1 _ ra)); rewrite dfb =>rd; move: (rd _ rb) => [qa qb qc]. rewrite (qc t rc) /h2 LfV// => //; exact (h1p' _ _ ra rb). have h3p3: forall x, inc x sPhi -> inc (h3 x) (permutations E). move => x xs; move: (proj1 (h3p1 _ xs)) => [ra rb rc]. apply/permutationsP; split => //; apply:bijective_if_same_finite_c_inj. rewrite rb rc //. rewrite rb; apply /NatP; rewrite cardE;fprops. split => // t1 t2 ; rewrite rb; move/pfa3 => [rd re] /pfa3 [rf rg]. move: (h3p2 _ _ _ xs re rd) (h3p2 _ _ _ xs rg rf) =>[pa pb][pc pd] eq1. move:(sphi_p1 _ xs) => [_ /permutationsP [[[fp ip] _] sp tp] xpb]. case: (equal_or_not (fc t1) (fc t2)) => eq2; last first. rewrite - sp in re rg; case: eq2; apply: (ip _ _ re rg). have sa: inc (Vf (P x) (fc t1)) In by Wtac. have sb: inc (Vf (P x) (fc t2)) In by Wtac. rewrite - eq1 in pd; exact: (pfa2 _ _ _ sa pb sb pd). move: eq1; rewrite pa pc - eq2 /h1. rewrite - eq2 in rf. have sb: inc (Vg (Q x) (fc t1)) (permutations Iq) by apply: xpb. move: sb; set sig0 := (Vg (Q x) (fc t1)); move /permutationsP=> [ua ub uc]. move: (fibig _ re) => [[[sa' sb'] _] sd' se'] => h. rewrite sd' in sb'; apply: (sb' t1 t2 rd rf). have t1as: inc (Vf (fi (fc t1)) t1) (source sig0) by rewrite ub; Wtac. have t2as: inc (Vf (fi (fc t1)) t2) (source sig0) by rewrite ub; Wtac. apply: (proj2 (proj1 ua) _ _ t1as t2as). have: inc (Vf (P x) (fc t1)) In by Wtac. move /(fibig) /inverse_bij_bp => [[[_ sa''] _ ] sb'' _]. apply: sa'' => //; rewrite sb''; Wtac; fct_tac. set TT := Zo _ _. have h3p4: forall x i, inc x sPhi -> inc i In -> (Vf (extension_to_parts (h3 x)) (Vg fb i)) = (Vg fb (Vf (P x) i)). move => x i xs iN. move: (proj1 (h3p1 _ xs)) => [fh3 sh3 th3]. have pb: sub (Vg fb i) (source (h3 x)) by rewrite sh3; exact: (pfa1 i iN). rewrite (etp_V (proj31 fh3) pb). set_extens t. move => /(Vf_image_P fh3 pb) [u ua ->]. exact:(proj2 (h3p2 _ _ _ xs iN ua)). move => ta; apply/(Vf_image_P fh3 pb). move: (proj32 (sphi_p1 _ xs)) => /permutationsP [xa xb xc]. have tb: inc (Vf (P x) i) In by Wtac; fct_tac. pose u:= Vf (inverse_fun (h3 x)) t. have tc: inc t (target (h3 x)) by rewrite th3;exact (pfa1 _ tb _ ta). have td:bijection (h3 x) by move:(h3p3 _ xs) => /permutationsP []. have td':=(bijective_inv_f td). have uE: inc u E by rewrite - sh3 - ifun_t; apply:Vf_target; aw. move: (pfa3 _ uE) => [te tf]. have tv: t = Vf (h3 x) u by rewrite /u (inverse_V td tc). exists u => //. move: (h3p2 x (fc u) u xs tf te) => [tg th]; rewrite - tv in th. have tx:inc (Vf (P x) (fc u)) In by Wtac; fct_tac. move: (pfa2 t (Vf (P x) i) (Vf (P x) (fc u)) tb ta tx th) => www. by move: (proj2 (proj1 xa)); rewrite xb => ii; rewrite (ii _ _ iN tf www). have h3p5: forall x, inc x sPhi -> inc (h3 x) TT. move => x xs; move: (h3p3 _ xs) => hp; apply:Zo_i => //. move /permutationsP:hp => [bh3 sh3 th3]. have fh3: function (h3 x) by fct_tac. have pa: function (extension_to_parts (h3 x)) by apply: etp_f; fct_tac. have pb:sub p0 (source (extension_to_parts (h3 x))). rewrite lf_source sh3 //. move: (sphi_p1 _ xs) => [_ /permutationsP [wa wb wc] _]. rewrite /F /extension_p3; set_extens t. move/(Vf_image_P pa pb) => [ u up ->]. have [i iN <-]: exists2 i, inc i In & (Vg fb i) = u. have usa:inc u (source fa) by ue. exists (Vf fa u); first by Wtac; fct_tac. rewrite -/(Vf _ _) inverse_V2 //. rewrite (h3p4 _ _ xs iN) -/(Vf _ _) - sfa - ifun_t; Wtac. rewrite ifun_s tfa; Wtac; fct_tac. rewrite -{1} sfa => ts. have ->: t = Vg fb (Vf fa t) by rewrite -/(Vf _ _) (inverse_V2 bfa ts). move: (Vf_target (proj1 (proj1 bfa)) ts); rewrite tfa - wc => ra. move: (proj2 (proj2 wa) _ ra) => [y yt ->]; rewrite wb in yt. have rb:=(rfb' _ yt). by apply (Vf_image_P pa pb);ex_tac;rewrite (h3p4 _ _ xs yt). pose repi i := (Vf (inverse_fun (fi i)) \0c). have ra: forall i, inc i In -> inc (repi i) (Vg fb i). move=> i iN. move:(fibig _ iN) => [bfi sfi tfi]. have ifi:= bijective_inv_f bfi. rewrite /repi - sfi - ifun_t; apply: (Vf_target ifi); rewrite ifun_s tfi. by apply /(NintP qN). have h3p7:forall u v, inc u sPhi -> inc v sPhi -> h3 u = h3 v -> u = v. move => u v up vp sh3. move:(sphi_p1 _ up)(sphi_p1 _ vp) =>[pu pu1 pu2][pv pv1 pv2]. have rb: P u = P v. move/permutationsP:pu1 =>[btu stu ttu]. move/permutationsP:pv1 =>[btv stv ttv]. move: (proj1 (proj1 btu)) (proj1 (proj1 btv)) => fu fv. apply:(function_exten fu fv); try ue. rewrite stu => i iN. have qa:=(ra _ iN). move: (proj2 (h3p2 _ _ _ up iN qa)) (proj2 (h3p2 _ _ _ vp iN qa)). rewrite - sh3; set t := Vf _ _ => i1 i2. have i3:inc (Vf (P u) i) (domain fb) by rewrite dfb; Wtac. have i4:inc (Vf (P v) i) (domain fb) by rewrite dfb; Wtac. case: (proj32 pfa _ _ i3 i4) => // di; empty_tac1 t. apply:(pair_exten pu pv rb). move /setX_P: (up) => [_ _] /Zo_P [_][pu3 pu4]. move /setX_P: (vp) => [_ _] /Zo_P [_][pv3 pv4]. have pu5: domain (Q u) = domain (Q v) by ue. apply:(fgraph_exten pu3 pv3 pu5); rewrite - pu4 => i iN. move /permutationsP: (pu2 _ iN) => [qu1 qu2 qu3]. move /permutationsP: (pv2 _ iN) => [qv1 qv2 qv3]. have ss: source (Vg (Q u) i) = source (Vg (Q v) i) by rewrite qv2. have tt: target (Vg (Q u) i) = target (Vg (Q v) i) by rewrite qv3. apply: (function_exten (proj1 (proj1 qu1)) (proj1 (proj1 qv1)) ss tt). clear pu pv pv1 pu2 pu3 pu4 pu5 pu2 pv2 pv3 pv4 ss tt. rewrite qu2 => k kq. move:(fibig i iN) => [sa sb sc]. have sa':= (bijective_inv_f sa). set t := Vf (inverse_fun (fi i)) k. have ts: inc t (Vg fb i) by rewrite - sb /t - ifun_t; Wtac; aw; rewrite sc. move: (proj1 (h3p2 _ _ _ up iN ts)) (proj1 (h3p2 _ _ _ vp iN ts)). rewrite sh3 => ->; rewrite /h1 - rb. have ->: (Vf (fi i) t) = k by rewrite (inverse_V sa) // sc. have /fibig [se sf sg]: inc (Vf (P u) i) In. move/permutationsP: pu1 => [[[ff _] _] sf <-]; Wtac. move /(f_equal (Vf (fi (Vf (P u) i)))). rewrite !inverse_V // sg;Wtac;fct_tac. have h3p6: forall y, inc y TT -> exists2 x, inc x sPhi & y = h3 x. move => f /Zo_P [/permutationsP [bpf sfp tfp]];rewrite /F/extension_p3 => hf. have ff: function f by fct_tac. have ra': forall i, inc i In -> inc (Vf f (repi i)) E. move => i iN; have ria:= (pfa1 _ iN _ (ra _ iN)); Wtac. pose tau i := fc (Vf f (repi i)). have rb: forall i, inc i In -> inc (tau i) In. move => i iN; exact: (proj2 (pfa3 (Vf f (repi i)) (ra' _ iN))). have fef:=(etp_f (proj31 ff)). have p0s: sub p0 (source (extension_to_parts f)) by rewrite lf_source sfp. have rc: forall i, inc i In -> Vf (extension_to_parts f) (Vg fb i) = Vg fb (tau i). move => i iN; set x := LHS. have xp: inc x p0. have sa:inc (Vg fb i) p0 by apply: rfb'. by rewrite - hf; apply/(Vf_image_P fef p0s); ex_tac. have ss: inc x (source fa) by ue. move: (inverse_V2 bfa ss); set i1 := Vf fa x; rewrite /Vf -/fb => xv. have i1N:inc i1 In by rewrite /i1; Wtac; fct_tac. move: (proj32 pfa i1 (tau i)); rewrite dfb - xv => rc. have rd: sub (Vg fb i) (source f) by rewrite sfp; fprops. case:(rc i1N (rb _ iN)); first by move ->. move: (proj1 (pfa3 _ (ra' _ iN))) => xx du; empty_tac1 (Vf f (repi i)). rewrite xv /x (etp_V (proj31 ff) rd);apply/Vf_image_P => //. move: (ra _ iN)=> re; ex_tac. have rd: inc (Lf tau In In) (permutations In). have inf:finite_set In by apply /NatP; rewrite (card_Nint nN). apply/permutationsP; saw;apply:bijective_if_same_finite_c_inj;aw; trivial. apply:(lf_injective rb) => u v ui vi sv. have hx i: inc i In -> inc (Vg fb i) (source (extension_to_parts f)). by rewrite lf_source sfp => iN; apply:ha; apply: rfb'. move:(rc _ ui); rewrite sv -(rc _ vi) => sa. move: (proj2 (etp_fi (proj1 bpf)) _ _ (hx _ ui) (hx _ vi) sa). apply: (injfb _ _ ui vi). have re: forall i, inc i In -> lf_axiom (Vf f) (Vg fb i) (Vg fb (tau i)). move => i iN t ta. have sff: sub (Vg fb i) (source f) by rewrite sfp; apply: (pfa1 _ iN). rewrite - (rc _ iN) (etp_V (proj31 ff) sff);apply /(Vf_image_P ff sff). ex_tac. have rf: forall i, inc i In -> bijection (Lf (Vf f) (Vg fb i)(Vg fb (tau i))). move => i iN. have cs:=(he _ (rfb' _ iN)). have cc: cardinal (Vg fb i) = cardinal (Vg fb (tau i)). by rewrite cs he //; apply:rfb'; apply: rb. have fss:finite_set (Vg fb i) by apply /NatP; rewrite cs. have ax:= (re _ iN). apply:bijective_if_same_finite_c_inj; aw; trivial. have sff: sub (Vg fb i) (source f) by rewrite sfp; apply: (pfa1 _ iN). by apply: lf_injective =>// u v /sff us /sff vs;apply:(proj2 (proj1 bpf)). pose si i s := (Vf (fi (tau i)) (Vf f (Vf (inverse_fun (fi i)) s))). pose s' i:= ((fi (tau i) \co Lf (Vf f) (Vg fb i) (Vg fb (tau i))) \co inverse_fun (fi i)). have sia: forall i s, inc i In -> inc s Iq -> [/\ (bijection_prop (s' i) Iq Iq), si i s = Vf (s' i) s & inc (si i s) Iq]. move => i s iI sS; rewrite /s';set f' := Lf _ _ _. move:(fibig _ iI) (fibig _ (rb _ iI))(rf _ iI) => [qa qb qc][qd qe qf] qg. have qh: source f' = (Vg fb i) by rewrite lf_source. have qi: target f' = (Vg fb (tau i)) by rewrite lf_target. have pa:inc s (target (fi i)) by rewrite qc. have pb':function (fi (tau i)) by fct_tac. have pb'':function f' by fct_tac. have pb: fi (tau i) \coP f' by hnf;rewrite qe qi. have pc: function (fi (tau i) \co f') by fct_tac. have pd':=(bijective_inv_f qa). have pd:(fi (tau i) \co f') \coP inverse_fun (fi i). hnf; aw; rewrite qh qb; split => //. have pe:inc (Vf (inverse_fun (fi i)) s) (source f'). by rewrite qh - qb - ifun_t; Wtac; aw. have pe':inc (Vf (inverse_fun (fi i)) s) (Vg fb i) by rewrite - qh. have pf := (re _ iI). have ba:=(compose_fb (inverse_bij_fb qa) (compose_fb qg qd pb) pd). split; first by hnf; aw; rewrite qc qf. by rewrite /f' ! compfV// ? LfV//; aw. by rewrite /si; Wtac; rewrite qe; apply:pf. have sax i:inc i In -> lf_axiom (si i) Iq Iq. move => iN t ts; exact:(proj33 (sia _ _ iN ts)). have sib: forall i, inc i In -> inc (Lf (si i) Iq Iq) (permutations Iq). move => i iN; apply /permutationsP; hnf; saw. have zq: inc \0c Iq by apply/(NintP qN). have [sa sb sc]:= (proj31 (sia _ _ iN zq)). have -> //: (Lf (si i) Iq Iq) = s' i. have ax:= (sax _ iN). have sd: function (Lf (si i) Iq Iq) by apply:(lf_function ax). apply:function_exten; [ exact | fct_tac | by rewrite lf_source | |]. by rewrite lf_target. rewrite lf_source => s sq; rewrite LfV//; exact:(proj32 (sia _ _ iN sq)). pose x := J (Lf tau In In) (Lg In (fun i => (Lf (si i) Iq Iq))). have xphi: inc x sPhi by apply:(setXp_i rd); apply: gfunctions_i1. ex_tac. move:(proj1 (h3p1 _ xphi)) => [qa qb qc]. apply:(function_exten ff qa); [ by rewrite qb | by rewrite qc | ]. move => y /=; rewrite sfp => yE. move:(pfa3 y yE)=> [qd qe]. move:(fibig _ qe) => [qf qg qh]. move:(fibig _ (rb _ qe)) => [qf' qg' qh']. have qi: inc y (source (fi (fc y))) by ue. have qj:inc (Vf (fi (fc y)) y) Iq by Wtac; fct_tac. move: (re _ qe _ qd); rewrite - qg' => qj'. rewrite (proj1 (h3p2 _ _ _ xphi qe qd)) /h1 /x pr1_pair pr2_pair. rewrite (LfV rb qe) (LgV qe) (LfV (sax _ qe) qj) /si (inverse_V2 qf qi). by rewrite (inverse_V2 qf' qj'). pose Phi:= Lf h3 sPhi TT. symmetry; apply/card_eqP; exists Phi; split;rewrite /Phi;aw; trivial. by apply: lf_bijective. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)