proposition: Lemma Exercise5_5_a2 I: sub I E -> nonempty I -> finite_set I -> Exercise5_5_conc I.
proof: Proof. move => IE neI fsi. set m := cardinal I. have mN: natp m by apply /NatP. have mz: m <> \0c by move:(card_nonempty1 neI). move: (card_Nintcp mN mz); move /card_eqP. move: (cpred_pr mN mz) => [pa pb]. move => [G [bG sG tG]]. have fg: function G by fct_tac. set K := Nintc (cpred m). pose g x := Vf G x. have aux: forall x, inc x K -> inc (g x) E. rewrite /K - sG; move => x xk; apply: IE; rewrite - tG /g; Wtac. move: (Exercise5_5_a1 pa aux). rewrite /Exercise5_5_conc_aux /Exercise5_5_conc. have ->:(fun_image (Nintc (cpred m)) g) = I. rewrite - sG - tG;set_extens t. move /funI_P; rewrite /g; move => [z za ->]; Wtac. move => tg; move: (bij_surj bG tg) => [x xs ->]. apply /funI_P; ex_tac. have ga: forall t, sub t (source G) -> sub (fun_image t g) I. move => t tg s /funI_P [z zt ->]; rewrite -tG /g; Wtac. have gb: forall t, sub t (source G) -> cardinal t = cardinal (fun_image t g). move => t tg; symmetry; apply cardinal_fun_image. move => u v ut vt sg; move: (tg _ ut) (tg _ vt) => ug vg. apply: (bij_inj bG ug vg sg). have gc: forall u v, sub u (source G) -> sub v (source G) -> fun_image u g = fun_image v g -> u = v. move => u v us vs sf; set_extens t => tu. have : inc (g t) (fun_image v g) by rewrite - sf; apply: funI_i. move /funI_P => [z za zb]. by rewrite (bij_inj bG (us _ tu)(vs _ za) zb). have : inc (g t) (fun_image u g) by rewrite sf; apply: funI_i. move /funI_P => [z za zb]. by rewrite (bij_inj bG (vs _ tu) (us _ za) zb). have gd: forall u, sub u I -> exists2 t, sub t (source G)& (fun_image t g) =u. move => u uI; exists (Zo (source G) (fun z => inc (g z) u)). by apply: Zo_S. set_extens t; first by move => /funI_P [z ] /Zo_P [] _ h ->. rewrite -tG in uI; move => tu; move: (bij_surj bG (uI _ tu)) => [x p1 p2]. apply /funI_P; rewrite p2 /g; exists x => //; apply: Zo_i => //; ue. have ra: quasi_bij(fun_image^~ g)(even_card0_sub (source G)) (even_card0_sub I). split. + move => t /Zo_P [] /Zo_P [] /setP_P t1 t2 /set1_P te. apply /Zo_P; split. apply /Zo_P; split; first by apply /setP_P; fprops. by rewrite - (gb _ t1). apply /set1_P => e; case: (emptyset_dichot t) => //; move => [s st]. by empty_tac1 (g s); apply: funI_i. + move => u v /Zo_P [] /Zo_P [] /setP_P h1 _ _. by move => /Zo_P [] /Zo_P [] /setP_P h2 _ _; apply: gc. + move => y /Zo_P [] /Zo_P [] /setP_P p1 p2 p3. move: (gd _ p1) => [t t1 t2]; exists t => //; apply /Zo_P; split. apply /Zo_P; split; first by apply/setP_P. by rewrite (gb _ t1) t2. move /set1_P => h1; case: p3; apply /set1_P; rewrite -t2. by rewrite h1; apply /set0_P => s /funI_P [z] /in_set0. rewrite - sG (csum_Cn2 _ ra) => ->. symmetry;apply: csum_Cn2; split. + move => t /Zo_P [] /setP_P p1 p2; apply /Zo_P;rewrite - (gb _ p1);split=> //. apply /setP_P; fprops. + by move => u v /Zo_P [] /setP_P us _ /Zo_P [] /setP_P vs _; apply: gc. + move => y /Zo_P [] /setP_P p1 p2; move: (gd _ p1) => [t t1 t2]. exists t => //; apply /Zo_P; split; first by apply /setP_P. by rewrite (gb _ t1) t2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)