proposition: Lemma Exercise5_5_b3 I (f: fterm) : finite_set I -> cardinal (unionf I f) +c csumb (even_card0_sub I) (fun z => cardinal (intersectionf z f)) = csumb (odd_card_sub I) (fun z => cardinal (intersectionf z f)).
proof: Proof. case: (emptyset_dichot I). move => ->; rewrite setUf_0 cardinal_set0. have ->: (even_card0_sub emptyset) = emptyset. by apply /set0_P => t /setC1_P [] /Zo_S /setP_P /sub_set0 h. have ->: (odd_card_sub emptyset) = emptyset. apply /set0_P => t /Zo_P [] /setP_P/sub_set0 ->. by rewrite cardinal_set0 => /odd_zero. rewrite csum0l //; apply:CS_cardinal. move => neI fse. set m := cardinal I. have mN: natp m by apply/NatP. have mz: m <> \0c by apply:card_nonempty1. move:(card_Nintcp mN mz); move /card_eqP. move: (cpred_pr mN mz); set n := cpred m; move=> [pa pb] [G [bG sG tG]]. have fg: function G by fct_tac. pose g i := f (Vf G i). set A := unionf I f; set E := \Po A;set r:= subp_order A. have esr: E = substrate r by symmetry; apply: (proj2 (subp_osr A)). have lr: lattice r by apply: setP_lattice. move: (@setP_lattice_d1 A) => dl1. have cf: forall x, inc x E -> cardinalp (cardinal x) by move => x _; fprops. have fp: forall x y, inc x E -> inc y E -> cardinal x +c cardinal y = cardinal (sup r x y) +c cardinal (inf r x y). move => x y xe ye; move: (setP_lattice_pr xe ye) => [-> ->]. apply: Exercise5_5_b1. have pc: (forall i, inc i (Nintc n) -> inc (g i) E). rewrite - sG => i iG; move: (Vf_target fg iG); rewrite tG => h. apply /setP_P => s sa; apply /setUf_P; ex_tac. move: (Exercise5_5_a1 lr dl1 esr cf fp pa pc). rewrite /Exercise5_5_conc_aux. set J := (Nintc n). have pd: sub (fun_image J g) (\Po A). by move => t /funI_P [z za zb]; move: (pc _ za); rewrite zb. move: (setU_sup pd) => h; rewrite - (supremum_pr2 (proj1 lr) h). have pe: forall x, sub x J -> (fun_image x g) = fun_image (Vfs G x) f. rewrite /J - sG; move => x xJ. set_extens t => /funI_P [z za ->]; apply /funI_P. exists (Vf G z) => //; apply/ (Vf_image_P fg xJ); ex_tac. move /(Vf_image_P fg xJ): za => [u ux ->]; ex_tac. have ->: (fun_image J g) = fun_image I f. by rewrite -tG - (surjective_pr0 (proj2 bG)) /Imf sG; apply: pe. have ->: union (fun_image I f) = A. set_extens t. move /setU_P => [z tz] /funI_P [u ui uv]; apply /setUf_P; ex_tac; ue. by move/setUf_P => [y yi tf]; apply /setU_P; exists (f y) => //; apply:funI_i. have pf: forall x, inc x (\Po J) -> nonempty x -> (infimum r (fun_image x g)) = intersectionf (Vfs G x) f. move => x /setP_P qa qb. have ta: nonempty (fun_image x g) by apply: funI_setne. have tb: sub (fun_image x g) (\Po A). by move => t /funI_P [z zx ->]; apply: pc; apply: qa. move: (ta); rewrite {1} (pe _ qa) => ta1. have tc: nonempty (Vfs G x). by apply /nonemptyP => ba; move: ta1; rewrite ba funI_set0 => /nonemptyP. move: (setI_inf tb); Ytac0 => h1; rewrite - (infimum_pr2 (proj1 lr) h1). rewrite (pe _ qa); set_extens t. move /(setI_P ta1) => hi; apply: (setIf_i tc) => j ja. by apply: hi; apply: funI_i. move /(setIf_P _ tc) => hi;apply: (setI_i ta1) => j /funI_P [z za ->]. by apply: hi. have pg: forall s, sub s J -> sub (Vfs G s) I. by rewrite -tG; move => s sj; apply: fun_image_Starget1. have ph: forall s, sub s J -> cardinal (Vfs G s) = cardinal s. move => s sj; symmetry;apply /card_eqP. apply Eq_restriction1;[ ue | exact (proj1 bG)]. have pi: forall u v, sub u J -> sub v J -> Vfs G u = Vfs G v -> u = v. rewrite /J - sG; move => u v uJ vJ si; set_extens t => tu. have : inc (Vf G t) (Vfs G v). rewrite - si; apply /(Vf_image_P fg uJ); ex_tac. move /(Vf_image_P fg vJ) => [w wv] sv. by rewrite (bij_inj bG (uJ _ tu) (vJ _ wv) sv). have : inc (Vf G t) (Vfs G u). by rewrite si; apply /(Vf_image_P fg vJ); ex_tac. move /(Vf_image_P fg uJ) => [w wv] sv. by rewrite (bij_inj bG (vJ _ tu)(uJ _ wv) sv). have pj: forall y, inc y (\Po I) -> exists x, [/\ inc x (\Po J), Vfs G x = y & cardinal x = cardinal y]. move => y /setP_P; rewrite - tG => yG; rewrite /J - sG. set x := Zo (source G) (fun z => inc (Vf G z) y). have xj: sub x (source G) by apply: Zo_S. have xj': sub x J by rewrite /J - sG. exists x; rewrite - (ph _ xj'). suff : Vfs G x = y by move => ->; split => //; apply /setP_P. set_extens t. by move /(Vf_image_P fg xj) => [u] /Zo_P [_] hh ->. move => ty; apply /(Vf_image_P fg xj); move: (bij_surj bG (yG _ ty)). by move => [a ag eq]; exists a => //; apply /Zo_P; rewrite - eq. clear h. set A1 := even_card0_sub _; set A2 := even_card0_sub _. have qx: quasi_bij (Vfs G) A1 A2. split. + move => s /Zo_P [] /Zo_P [] /setP_P sj a1 /set1_P a2. move: (pg _ sj) (ph _ sj) => s1 s2. apply /Zo_P; split. by apply /Zo_P;rewrite s2;split => //; apply/setP_P. move /set1_P => s3; case: (emptyset_dichot s) => // [] [t ts]. empty_tac1 (Vf G t); apply /Vf_image_P => //; [ ue | ex_tac]. + move => u v /Zo_P [] /Zo_P [] /setP_P uJ _ _. by move => /Zo_P [] /Zo_P [] /setP_P vJ _ _; apply: pi. + move => t /Zo_P [] /Zo_P [t1 t2] /set1_P t3. move: (pj _ t1) => [x [x5 x6 x7]]. exists x => //; apply /Zo_P; split; first by apply /Zo_P; rewrite x7. by move /set1_P => xe; move: x6; rewrite xe fun_image_set0; apply: nesym. have <- : csumb A2 (fun z => cardinal (intersectionf z f)) = csumb A1 (fun z => cardinal (infimum r (fun_image z g))). rewrite (csum_Cn2 _ qx); apply: csumb_exten. move => s sa; move /Zo_P: (sa) => [] /Zo_P [sb sc] /set1_P sd. by rewrite pf //; apply /nonemptyP. move ->; clear qx A1 A2. have qx: quasi_bij (Vfs G) (odd_card_sub J) (odd_card_sub I). split. + move => s /Zo_P [] /setP_P sj a1; move: (pg _ sj) (ph _ sj) => s1 s2. by apply /Zo_P; rewrite s2;split => //; apply/setP_P. + by move => u v /Zo_P [] /setP_P uJ _ /Zo_P [] /setP_P vJ _; apply: pi. + move => y /Zo_P [t1 t2]; move: (pj _ t1) => [x [x5 x6 x7]]. exists x => //; apply /Zo_P; rewrite x7;split => //. symmetry; rewrite (csum_Cn2 _ qx); apply: csumb_exten => s sa. by move /Zo_P: (sa) => [sc sd]; move: (odd_nonempty sd) => nes; rewrite pf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)