proposition: Lemma Saleph_square E: Saleph E -> E \Eq (E \times E).
proof: Proof. move => [einf [r [wor sr]]]; move:(proj1 wor) => or. have H a b : a \Is b -> (substrate a) \Eq (substrate b). by move =>[f [_ _ fp _]]; exists f. move:Nat_order_wor => [wor2 sr2]. move:(EqS equipotent_N2_N) => resa. have Hu x y: x \Eq (coarse x) -> x \Eq y -> y \Eq (coarse y). move => ha hb; exact: (EqT (EqS hb) (EqT ha (Eq_mul_inv hb hb))). case: (p_or_not_p (Nat \Eq E)) => ne. move: ne =>[f fp]; have ne: Nat \Eq E by exists f. exact: (Hu _ _ resa ne). case:(isomorphism_worder2 wor2 wor). by move /H; rewrite sr sr2. move =>[x];rewrite sr2; move:(@sub_segment Nat_order x) => qa qb. move/H; rewrite (iorder_sr (proj1 wor2) qa); rewrite sr => /EqS hh. case:einf; split; last by move => rn1; case: ne; apply: EqS. apply/set_leP; exists (segment Nat_order x) => //; ue. move =>[x0]; rewrite sr; move:(@sub_segment r x0). set S0 := (segment r x0) =>S0E xE is1. move: is1 =>[f1 [_ _ fp _]]; move: fp;rewrite (iorder_sr or S0E) sr2 => fp. pose a0 := Vf (inverse_fun f1) C0. pose a1 := Vf (inverse_fun f1) C1. move:(fp) => [qa qb qc]. have ha: inc C0 (target f1) by rewrite qc; apply: NS0. have hb: inc C1 (target f1) by rewrite qc; apply: NS1. move:(inverse_Vis qa ha) (inverse_Vis qa hb); rewrite qb -/a1 -/a0 => a0S0 a1S1. have aneb: a0 <> a1. move => /(f_equal (Vf f1)). rewrite (inverse_V qa ha) (inverse_V qa hb); fprops. clear qa qb qc ha hb. have qa: S0 \Eq Nat by exists f1. move:(Hu _ _ resa (EqS qa)) =>[f0 f0p]. rewrite sr in S0E. clear fp qa ne resa einf. pose Gi g := forall y, singl_val (fun x => inc (J x y) g). pose T0 := \Po (E \times (E\times E)). pose pra G := [/\ fgraph G, Gi G, range G = coarse (domain G), segmentp r (domain G) & sub S0 (domain G)] . pose prb f:= [/\ bijection_prop f (source f) (coarse (source f)), segmentp r (source f) & sub S0 (source f)]. have ra f: prb f -> pra (graph f). move =>[[[fi fs ] sf tf] ssf xp]; hnf. have gig: Gi (graph f) by move => y; apply: (injective_pr3 fi). move:(proj1 fi) => ff; move: (function_fgraph ff) => fgf. rewrite (domain_fg ff). move: (surjective_pr0 fs); rewrite (ImfE ff) => ->; rewrite -tf; done. have ra' f: sub (source f) E -> prb f -> inc (graph f) T0. move => hu [[bf sf tf] hb hc]; apply/setP_P. have ff := (proj1 (proj1 bf)). move: (sub_graph_setX (proj1 (function_fgraph ff))). rewrite (domain_fg ff) => hyp t /hyp /setX_P[pt r1 r2]. apply/setX_P; split => //; first by apply: hu. move: r2; rewrite - (ImfE ff) => r3; move: (Imf_Starget ff r3); rewrite tf. by move => /setX_P [pu r4 r5]; apply/setX_P; split => //; apply: hu. pose Fg g := (triple (domain g) (range g) g). have rb g: pra g -> prb (Fg g). rewrite/Fg; move =>[qa qb qc qd qe]; hnf; saw. rewrite /bijection_prop; aw; rewrite - qc; split => //. have ff: function (triple (domain g) (range g) g). apply: function_pr => //. split; first by apply: (injective_pr_bis ff); aw. by apply: (surjective_pr1 ff); rewrite (ImfE ff); aw. have rb' g: inc g T0 -> sub (source (Fg g)) E. by move => /setP_P h; rewrite /Fg; aw => t /funI_P [z /h /setX_P [_ zz _] ->]. pose T1 := Zo T0 pra. have neT: inc (graph f0) T1. move: (f0p) =>[bf sf tf]. have h: (prb f0) by rewrite /prb sf; split => //; apply:segment_segment. by apply: Zo_i; [ apply: (ra' f0 _ h); ue | apply: ra]. pose tot X := total_order (induced_order (sub_order T1) X). have rc: forall X, sub X T1 -> nonempty X -> tot X -> inc (union X) T1 /\ forall y, inc y X -> sub y (union X). move => X ha hb hc; split; last first. move => y yX t yx; union_tac. apply: Zo_i. by apply/setP_P => t /setU_P [u uy /ha /Zo_S /setP_P h]; apply: h. have to u v: inc u X -> inc v X -> sub u v \/ sub v u. move:(sub_osr T1) =>[sa sb]. have sc: sub X (substrate (sub_order T1)) by rewrite sb. move => ux vx; move: (proj2 hc u v); rewrite (iorder_sr sa sc) => sd. move:(sd ux vx); case; move=> /iorder_gle1 /sub_gleP; case; auto. move: (domain_setU X) => dx. have res4: segmentp r (domain (union X)). rewrite dx; apply: setU_segment =>t/funI_P [z zX ->]. by move:(ha _ zX) => /Zo_hi []. have res5: sub S0 (domain (union X)). move: hb => [x xX];move:(ha _ xX) => /Zo_hi [_ _ _ _] ss. apply: (sub_trans ss). by rewrite dx => t ts;apply/setU_P; exists (domain x) => //; apply: funI_i. have res3: range (union X) = coarse (domain (union X)). rewrite dx range_setU; set_extens t. move => /setU_P[y ry /funI_P[z zx zv]]. move:(ha _ zx) => /Zo_hi[_ _ rx _ _]. have: sub (domain z) (union (fun_image X domain)). by move => s sd; apply/setU_P; exists (domain z) => //; apply: funI_i. by move/ setX_Sll; apply; rewrite -rx - zv. move => /setX_P [pt t1 t2]. move: t1 => /setU_P[x1 x1v /funI_P [y1 y1X y1v]]. move: t2 => /setU_P[x2 x2v /funI_P [y2 y2X y2v]]. case: (to _ _ y1X y2X) => ss. apply/setU_P; exists (range y2); last by apply: funI_i. move:(ha _ y2X) => /Zo_hi [_ _ -> _ _]; apply/setX_P. split; [ exact | apply:(domain_S ss); ue | ue ]. apply/setU_P; exists (range y1); last by apply: funI_i. move:(ha _ y1X) => /Zo_hi [_ _ -> _ _]; apply/setX_P. split; [ exact | ue | apply:(domain_S ss); ue ]. have res1: fgraph (union X). split. by move => t/setU_P [y ty /ha/Zo_hi [[hu _] _ _ _ _]]; apply: hu. move => u v /setU_P [x tx xX] /setU_P [y ty yX] sp. move: (xX) (yX) => /ha/Zo_hi [[_ hx] _ _ _ _] /ha/Zo_hi [[_ hy] _ _ _ _]. case: (to _ _ xX yX) => ss. by apply: hy => //; apply: ss. by apply: hx => //; apply: ss. have res2: Gi (union X). move => z u v /setU_P [x tx xX] /setU_P [y ty yX]. move: (xX) (yX) => /ha/Zo_hi [_ hx _ _ _] /ha/Zo_hi [_ hy _ _ _]. case: (to _ _ xX yX) => ss. by apply: (hy z) => //; apply: ss. by apply: (hx z) => //; apply: ss. done. move:(sub_osr T1) =>[orT1 srT1]. pose max x := Yo (x = emptyset) (graph f0) (union x). have max_prop s: sub s (substrate (sub_order T1)) -> worder (induced_order (sub_order T1) s) -> upper_bound (sub_order T1) s (max s). rewrite srT1 => st wot1; rewrite /max; Ytac se. by split; [ rewrite srT1| rewrite se => y /in_set0]. move /nonemptyP: se => se. move: (rc s st se (worder_total wot1)) =>[qa qb]; split; first by ue. by move => y ys; move: (st _ ys)(qb _ ys) => qc qd; apply/sub_gleP. case: (all_exists_dichot2 (fun t => (domain t) \Eq E) T1); last first. move =>[f /Zo_P [qa qb]]. move:(rb _ qb) =>[]; rewrite /Fg; aw; set g := triple _ _ _ => bg _ _ ee. have eq1: (domain f) \Eq (coarse (domain f)) by exists g. apply:(Hu _ _ eq1 ee). move => T1_small. pose iorc x := (induced_order r (E -s x)). pose isof x := (iso_seg_fun (induced_order r (domain x)) (iorc (domain x))). pose na x := bij_double_F2_fun (domain x) (target (isof x)) a0 a1 (Fg x) (isof x). suff rd x: inc x T1 -> inc (graph (na x)) T1 /\ ssub x (graph (na x)). have next_prop x: inc x (substrate (sub_order T1)) -> glt (sub_order T1) x (graph (na x)). rewrite srT1 => xt1; move: (rd _ xt1) =>[qa [qb qc]]. by split=> //;apply/sub_gleP. by case:(Zorn_aux_eff orT1 max_prop next_prop). move => xT1. move:(T1_small x xT1) => noti. move/Zo_P: (xT1) =>[/setP_P sX xp]. move: (rb _ xp) =>[bp _ _];move: bp; rewrite {2 3} /Fg; aw => bp. move: xp => [_ _ _ sdx ss ]. have sdE: sub (domain x) (substrate r). by move => t /funI_P [z /sX /setX_P[_ ok _] -> ]; rewrite sr. have iaf: inc a0 (domain x) by apply: ss. have ibf: inc a1 (domain x) by apply: ss. move: (induced_wor wor sdE) => wo1. have scE: sub (E -s (domain x)) (substrate r). by move => y /setC_P; rewrite sr; case. move: (induced_wor wor scE); rewrite -/(iorc _) => wo2. set rF := (induced_order r (domain x)). set rG := (iorc (domain x)). move: (iorder_sr or sdE) (iorder_sr or scE) => sru srv. case: (isomorphism_worder_exists_v1 wo1 wo2); last first. set F := inverse_fun _. move =>[[qa _] [_ _ /inverse_bij_bp qb _]]. rewrite sru in qa. have st:= (sub_trans qa sdE). have eq2: (domain x) \Eq (coarse (domain x)) by exists (Fg x). move: qb; rewrite srv (iorder_trans _ qa) (iorder_sr or st) => eea. have eqe: (target F) \Eq (substrate r -s domain x). by rewrite sr; exists (inverse_fun F). by case: noti; move:(Eq_F_doubleE iaf ibf aneb qa sdE eq2 eqe); rewrite sr. set f := iso_seg_fun _ _. move => [qa [_ _ qb _]]. move:(proj1 qa); rewrite srv => qc. have qd: sub (target f) (substrate r). by rewrite sr; move => t / qc /setC_P; case. move: qb; rewrite sru /iorc (iorder_trans _ qc) (iorder_sr or qd) => qb. have di: disjoint (domain x) (target f). by apply:disjoint_pr => t tdx / qc /setC_P []. move:(bij_double_F2 iaf ibf aneb di bp qb). simpl; rewrite -/(na x). move => [hp1 hp2]. have sh: source (na x) = (domain x \cup target f) by case: hp1. have s0H: sub S0 (source (na x)). by rewrite sh;move => y / ss yd; apply:setU2_1. have sdhE: sub (source (na x)) E by rewrite sh - sr; apply: setU2_12S. have ssh: segmentp r (source (na x)). split; [ by rewrite sr | rewrite sh ]. move => a b /setU2_P ai lba; case: ai => ai. apply: setU2_1;exact:(proj2 sdx _ _ ai lba). case: (inc_or_not b (domain x)) => bdx; first by apply: setU2_1. have ad: inc a (E -s domain x). by apply/setC_P;split;[rewrite - sr; order_tac | move=> ad; empty_tac1 a]. have snd: inc b (E -s domain x). apply/setC_P; split => //; rewrite - sr; order_tac. have le1: gle (iorc (domain x)) b a by apply/iorder_gleP. apply: setU2_2; exact: (proj2 qa a b ai le1). rewrite - sh in hp1. have prbh: prb (na x) by []. have ht1: inc (graph (na x)) T1 by apply: Zo_i; [ apply: ra' | apply: ra]. split => //. split; first by move:(proj43 hp2); rewrite /Fg; aw. have fh: function (na x) by move: hp1 => [[[]]]. move => sg; move:(f_equal domain sg); rewrite domain_fg // sh => bad. move: qb => [[[ff _] _]sf tf]. have asf: inc a0 (source f) by rewrite sf. move:(Vf_target ff asf) => utf. have udx: (inc (Vf f a0) (domain x)) by rewrite bad; apply: setU2_2. empty_tac1 (Vf f a0). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)