proposition: Theorem equipotent_inf2_inf E: infinite_c E -> E ^c \2c = E.
proof: Proof. move=> ciE; move: (ciE) => [cE ioE]. have H F: cardinal F = (cardinal F) *c (cardinal F) <-> (F \Eq (coarse F)). rewrite /coarse cprod2cl cprod2cr cprod2_pr1; exact:card_eqP. have cEE:cardinal E = E by apply: card_card. have isE:infinite_set E by hnf; rewrite cEE. set (base := sub_functions E (coarse E)). pose pr z := injection z /\ Imf z = coarse (source z). have [psi [psibase prpsi ispsi]]: exists psi, [/\ inc psi base, pr psi & infinite_set (source psi)]. have [F [FE cFN]] := (infinite_greater_countable isE). have [f [bf sf tf]]: (F \Eq (coarse F)). apply/H;rewrite cFN aleph0_pr1; apply/H /EqS/equipotent_N2_N. have ff: function f by fct_tac. have pm: (sub (target f) (coarse E)) by rewrite tf; apply: setX_Slr. move: (change_target_pr ff pm); set y := (change_target_fun _ _). move => [[fy sy ty] yv]. exists y; rewrite /base sy sf; split => //. by apply /sfunctionsP; split => //; rewrite sy sf. split; last first. rewrite sy sf -tf -(surjective_pr0 (proj2 bf)). by rewrite (ImfE ff) (ImfE fy) /y/change_target_fun corresp_g. split => // u v; rewrite sy => uf vf. by rewrite yv // yv //; apply: (bij_inj bf). by apply/infinite_setP; rewrite cFN; apply: CIS_aleph0. set (odr := opp_order (extension_order E (coarse E))). set (ind := Zo base (fun z => pr z /\ sub (graph psi) (graph z))). have [oe se]:= (extension_osr E (coarse E)). have [oo soo] := (opp_osr oe). have so: sub ind (substrate odr) by rewrite soo se;apply: Zo_S. have [oi soi] := (iorder_osr oo so). have ii: inductive (induced_order odr ind). move => X; rewrite (iorder_sr oo so) => Xind. have aux1 := (sub_trans Xind so). rewrite (iorder_trans _ Xind)/total_order iorder_sr //; move => [iot tot]. case: (emptyset_dichot X)=> neX. exists psi; split; first by rewrite iorder_sr //; apply: Zo_i =>//; fprops. by rewrite neX; move=> u /in_set0. have [rx rxX]:= neX. have Hla:forall i, inc i X -> function i. by move => i /Xind /Zo_hi [[[ok _] _] _]. have Hlb:forall i, inc i X -> target i = coarse E. by move => i /Xind /Zo_S /sfunctionsP [_ _ h]. have Hlc: forall x y, inc x X -> inc y X -> gle odr x y \/ gle odr y x. move=> x y xX yX; case: (tot _ _ xX yX) => h;move: (iorder_gle1 h); fprops. set si := Lg X source. have Hd: forall i j, inc i (domain si) -> inc j (domain si) -> agrees_on ((Vg si i) \cap (Vg si j)) i j. rewrite /si;aw;move=> i j iX jX; rewrite !LgV//. split; [ apply: subsetI2l | by apply: subsetI2r |]. move=> a /setI2_P [asi asj]. by case: (Hlc _ _ iX jX)=> h; [ | symmetry ];apply: (extension_order_pr h). have He:forall i, inc i (domain si) -> function_prop i (Vg si i) (coarse E). rewrite /si Lgd => i iX; rewrite LgV //; split;fprops. move: (extension_covering He Hd). set x := common_ext _ _ _; rewrite/si Lgd ;move=> [[fx sx tx] agx _ etc]. have xb: inc x base. apply /sfunctionsP; split => // t; rewrite sx. move /setUb_P;aw; move=> [y yX]; move: (Xind _ yX). move => /Zo_S /sfunctionsP [_ pa _ ] ; rewrite LgV//; apply: pa. have Hg: forall i, inc i X -> sub (graph i) (graph x). move=> i iX. apply /(sub_functionP (Hla _ iX) fx). move: (etc _ iX); rewrite /agrees_on !LgV//;move=> [p1 p2 p3]; split => //. move=> a asi; symmetry; exact: p3. have sgp:(sub (graph psi) (graph x)). apply: sub_trans (proj2 (Zo_hi (Xind _ rxX))) (Hg _ rxX). have injx: injection x. split=>//; move => u v;rewrite sx. move => /setUb_P1 [a aX usa]/setUb_P1 [b bX vsb]. have [z [zX usz vsz]]: (exists z, [/\ inc z X, inc u (source z) & inc v (source z)]). by case: (Hlc _ _ aX bX); move /igraph_pP /extension_orderP => [_ _ /extends_Ssource h]; [exists b | exists a ]; split => //; apply: h. move: (etc _ zX); rewrite /agrees_on !LgV//;move => [_ _ aux]. rewrite (aux _ usz) (aux _ vsz). by move: (Zo_hi (Xind _ zX)) => [[[_ iz] _] _]; apply: iz. have rgx: Imf x = coarse (source x). set_extens a. move /(Imf_P (proj1 injx)) => [b bsx aW]; move: bsx. rewrite sx; move /setUb_P1=> [c cy bsc]. move: (etc _ cy); rewrite/agrees_on !LgV//;move => [_ _ aux]. rewrite (aux _ bsc) in aW. move: (Xind _ cy) => /Zo_hi [[ic rc] _]. have: inc a (coarse (source c)). by rewrite -rc aW; Wtac; move: bsc; aw. move /setX_P => [pa Ps Qs]; apply /setX_P. split => //; apply /setUb_P1; ex_tac. move => /setX_P [pa]; rewrite sx. move /setUb_P1 => [b bX psb] /setUb_P1 [c cX qsc]. have [z [zX usz vsz]]: (exists z, [/\ inc z X, inc (P a) (source z) & inc (Q a) (source z)]). by case: (Hlc _ _ bX cX); move /igraph_pP /extension_orderP => [_ _ /extends_Ssource h]; [exists c | exists b ]; split => //; apply: h. have :inc a (coarse (source z)) by apply /setX_i. move: (Xind _ zX) => /Zo_hi [[ic rc] _]. rewrite -rc; move /(Imf_P (proj1 ic)) => [d dsz ->]. move: (etc _ zX); rewrite/agrees_on !LgV//;move => [_ _ aux]. rewrite -(aux _ dsz); apply /(Imf_P fx); exists d => //. rewrite sx; apply /setUb_P1; ex_tac. have xi: (inc x ind) by apply: Zo_i. exists x;split; first by rewrite iorder_sr. move=> z zX; move: (Xind _ zX) => zi. move: (zi) => /Zo_S zb. apply /iorder_gle0P => //; apply /igraph_pP /extension_orderP;split => //. move: zb => /sfunctionsP [_ _ tz]; hnf; rewrite tx tz; split; fprops. move: (Zorn_lemma oi ii) => [x]. rewrite /maximal (iorder_sr oo so); move => [xi aux]. have maxp: forall u, inc u ind -> extends u x -> u = x. move=> u ui ue;apply: aux; apply /iorder_gle0P => //. move: (Zo_S ui) (Zo_S xi)=> ub xb. apply /igraph_pP /extension_orderP;split => //. clear aux ii. move: xi => /Zo_P [] /sfunctionsP [fx ssxE txE] [[ijx rgx] sgx]. set (F := source x); set b:= cardinal F. have binf:infinite_c b. have ss: (sub (source psi) (source x)). have fspi: function psi by move: prpsi=> [ip _]; fct_tac. move: (domain_S sgx); rewrite ! domain_fg //. move: (sub_smaller ss); rewrite -/F -/b => p1. by apply: (cle_inf_inf _ p1); apply /infinite_setP. have bsq: (b = b *c b) by apply/H; rewrite /F -rgx; apply: Eq_src_range. case: (equal_or_not b E) => bE; first by rewrite -bE cpowx2 =>//. have cb:= proj1 binf. have bltE: (b <c E) by split ; [rewrite - cEE; exact: (sub_smaller ssxE) |]. have b2b : b = b +c b. apply:cleA; first by apply: (csum_M0le _ cb). rewrite csum_nn cprodC. by move: (cprod_Meqle b (infinite_ge2 binf));rewrite - bsq. have [/cardinal_le_aux1 lbEF _]: (cardinal b <c (cardinal(E -s F))). case: (cleT_el (CS_cardinal (E -s F)) (CS_cardinal b)); last by done. move /(csum_Meqle b). by rewrite (card_card cb) (cardinal_setC ssxE) -b2b cEE => /(cltNge bltE). move:lbEF; move/(eq_subset_cardP b _) => /set_leP [Y syc /card_eqP cY]. set (Z:= F \cup Y). set (a1:= coarse F); set (a2 := F \times Y); set (a3 := Y \times Z). move: (card_card cb) => ccb. case: (finite_not_infinite _ binf). suff: (Y= emptyset). move => eq; move: cY; rewrite eq cardinal_set0 ccb => ->; exact finite_0. have dFY: disjoint F Y. by apply: disjoint_pr; move=> u uF uy; move: (syc _ uy) => /setC_P [_]. move: (csum2_pr5 dFY). rewrite -/Z -/b - (csum2cl _ Y) - (csum2cr _ Y) - cY ccb - b2b => cZ. have ca1: cardinal (a2 \cup a3) = b. have di: disjoint a2 a3. apply: disjoint_pr; move => t /setX_P [_ af _] /setX_P [_ ay _]. by move: (syc _ ay) => /setC_P [_]. rewrite (csum2_pr5 di) - (csum2cr a2) - (csum2cl a2) - 2! cprod2_pr1. rewrite - cprod2cr - cprod2cl -/b -(cprod2cl Y) - cY - (cprod2cr _ Z) cZ ccb. by rewrite -bsq -b2b. have pzz: (coarse Z = (coarse F) \cup (a2 \cup a3)). set_extens t. move /setX_P => [pt]; case /setU2_P => r1. by case /setU2_P => r2; [| apply: setU2_2]; apply: setU2_1 ;apply: setX_i. move => xx; apply: setU2_2; apply: setU2_2 ;apply: setX_i => //. case /setU2_P; first by apply: setX_Sll; apply: subsetU2l. case /setU2_P => /setX_P [pa pb pc]; apply /setX_P;split => //; try (by apply: setU2_1); (by apply: setU2_2). have dzz: (disjoint (coarse F) (a2 \cup a3)). hnf in dFY. apply: disjoint_pr; move=> u /setX_P [_ pF qF];case /setU2_P. move /setX_P => [_ _ qY]; empty_tac1 (Q u). move /setX_P => [_ pY _]; empty_tac1 (P u). have: (Y \Eq (a2 \cup a3)) by apply /card_eqP; rewrite - cY ca1. move=> [x0 [bx0 sx0 tx0]]. set (g:= triple Z (coarse E) ((graph x) \cup (graph x0))). have Hga: source g = Z by rewrite /g;aw. have Hgb:graph g = ((graph x) \cup (graph x0)) by rewrite /g;aw. have fx0: function x0 by fct_tac. have Hgd: range (graph g) = coarse (source g). move: bx0 => [_ sjx0]. rewrite Hga pzz - tx0 - rgx -(surjective_pr0 sjx0). by rewrite (ImfE fx0) (ImfE fx) - range_setU2 /g;aw. have Hhf: target g = coarse E by rewrite /g; aw. have Hge:domain (graph g) = (source g). rewrite Hgb Hga domain_setU2 !domain_fg // sx0 //. have ze: sub Z E. by move=> t /setU2_P []; [apply: ssxE | move /syc => /setC_P []]. have fg: function g. rewrite /g;apply: function_pr. apply: fgraph_setU2; fprops; rewrite !domain_fg // sx0; exact dFY. rewrite - Hgb Hgd /coarse Hga; apply: setX_Slr =>//. by rewrite -Hgb Hge Hga. rewrite - (ImfE fg) in Hgd. have ig: injection g. have aux1: forall a b c, inc (J a b) (graph x) -> inc (J c b) (graph x0) -> False. move=> u v w J1 J2; empty_tac1 v. rewrite /F - rgx (ImfE fx); ex_tac. rewrite -tx0; apply: (p2graph_target fx0 J2). apply: injective_pr_bis =>//; rewrite /related Hgb. move=> u v w; case /setU2_P => h1; case /setU2_P => h2. apply: (injective_pr3 ijx h1 h2). case: (aux1 _ _ _ h1 h2). case: (aux1 _ _ _ h2 h1). move: bx0 => [ijx0 _]; apply: (injective_pr3 ijx0 h1 h2). have sg: sub (graph x) (graph g) by rewrite Hgb;apply: subsetU2l. have gi: inc g ind. apply: Zo_i; first by apply /sfunctionsP; rewrite Hga; split => //. split => //; apply: sub_trans sgx sg. have egx: extends g x by rewrite /extends; split => //; rewrite txE Hhf; fprops. apply /set0_P; move=> y yY; move: (syc _ yY) => /setC_P [_ yF]. by case: yF; rewrite/F - (maxp _ gi egx) Hga; apply: setU2_2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)