proposition: Lemma Exercise4_6h h: E46_hp h -> E46_conc h.
proof: Proof. move=> hp; move: (Exercise4_6g hp) => [k [kN kh [C [pC cc altc]]]]. move: pC => [[pca pcc] pcb]. move: Exercise4_6a => [[oR sR] rR]. hnf in disdom. have tcp: forall x a b, inc x C -> inc a x -> inc b x -> [\/ a = b, glt E46_order_r a b | glt E46_order_r b a]. move=> x a b xC ax bx; case: (equal_or_not a b) => nab; first by in_TP4. have nba: b <> a by apply:nesym. move /total_subordersP: (altc _ xC) => [sxs [or]]. rewrite iorder_sr //; move => aux; move: (aux _ _ ax bx). by case => aux2; [constructor 2 | constructor 3]=> //;move:(iorder_gle1 aux2). have tcp1: forall i j, glt E46_order_r i j -> [/\ inc i (domain X), inc j (domain Y) & meet (Vg X i) (Vg Y j)]. move=> i j [leij nij]; move: leij;rewrite rR; move => [isR jsR]. case => h0 //. have tcp2: forall x, inc x C -> [\/ (exists2 i, inc i (domain X) & x = singleton i), (exists2 j, inc j (domain Y) & x = singleton j) | (exists i j, glt E46_order_r i j /\ x = doubleton i j)]. move=> x xC; move: (pcb _ xC) => xne. move: (xne) => [y yx]. case: (equal_or_not x (singleton y)) => xs. have: inc y (union C) by union_tac. rewrite pca sR /E46_u. case /setU2_P => yc; [constructor 1 | constructor 2 ]; ex_tac. have [z zx yz]: exists2 z, inc z x & y <> z. ex_middle bad; case: xs; apply set1_pr => // z zx. ex_middle ty; case: bad; exists z;fprops. have [i [j [ix jx ltij]]]: exists i j, [/\ inc i x, inc j x & glt E46_order_r i j]. case: (tcp _ _ _ xC yx zx); first (by contradiction); case => h0. by exists y, z. by exists z, y. move: (tcp1 _ _ ltij) => [iX jY _]. constructor 3; exists i, j; split => //. set_extens t; last by case /set2_P => ->. move => tx; case: (tcp _ _ _ xC tx ix); first by move => ->; fprops. by move => ti; move: (tcp1 _ _ ti) => [_ iY _]; empty_tac1 i; aw. case: (tcp _ _ _ xC jx tx); first by move => ->; fprops. by move => tj; move: (tcp1 _ _ tj) => [jX _]; empty_tac1 j; aw. move => ti tj; move: (tcp1 _ _ ti) (tcp1 _ _ tj) => [tX _ _] [_ tY _]. empty_tac1 t. pose xup x y:= forall i, ( (inc i (x \cap (domain X)) -> inc y (Vg X i) ) /\ (inc i (x \cap (domain Y)) -> inc y (Vg Y i))). pose f x := choose (fun y => xup x y). have fp1: forall x, inc x C -> xup x (f x). move=> x xc; apply: choose_pr; case: (tcp2 _ xc). move => [i idX ->]; exists (rep (Vg X i)); hnf. move=> j;split; move => /setI2_P [] /set1_P -> uu. by apply: rep_i;move: Xpr => [_ _ _ hh]; apply: hh. empty_tac1 i; apply /setI2_P;split => //. move => [i idX ->]; exists (rep (Vg Y i)); hnf. move=> j; split; move => /setI2_P [] /set1_P -> uu. by empty_tac1 i; aw. by apply: rep_i;move: Ypr => [_ _ _ hh]; apply: hh. move=> [i [j [ltij]]] ->; move: (tcp1 _ _ ltij) => [idx jdy mt]. exists (rep ((Vg X i) \cap (Vg Y j))). move: (rep_i mt) => /setI2_P; set r:= rep _; move=> [ra rb]. move => z;aw;split; move => /setI2_P [];case /set2_P => -> bad //. by empty_tac1 j; aw. by empty_tac1 i; aw. set B:= fun_image C f. have pa: (cardinal B) <=c (n +c h). have sjb: (surjection (Lf f C (fun_image C f))). apply: lf_surjective; first by move=> t ta; apply /funI_P; exists t. move=> y /funI_P //. move: (image_smaller (proj1 sjb)); rewrite (surjective_pr0 sjb). aw; rewrite -/B => l1; apply:(cleT l1). rewrite cc; apply: csum_Mlele => //; fprops. have pb: finite_set B. move: hp => [hN _ _ _]. hnf; apply /NatP; apply: (@NS_le_nat _ (n +c h)); fprops. have sBA: sub B A. move=> t /funI_P [z zC ->]; move: (fp1 _ zC) => fz. move: Xpr Ypr => [fgX _ rpX _][fgY _ rpY _]. have auxx: forall i y, inc i (domain X) -> inc y (Vg X i) -> inc y A. move=> i y id yv. suff: sub (Vg X i) A by apply. apply /setP_P; apply: rpX; apply /(range_gP fgX); ex_tac. have auxy: forall i y, inc i (domain Y) -> inc y (Vg Y i) -> inc y A. move=> i y id yv. suff : sub (Vg Y i) A by apply. apply /setP_P; apply: rpY; apply /(range_gP fgY); ex_tac. case: (tcp2 _ zC). move=> [i idx zi]. have ii2: inc i (z \cap (domain X)) by rewrite zi; fprops. move: (fz i) => [fa _]; move: (fa ii2) => fv; apply: (auxx _ _ idx fv). move=> [i idx zi]. have ii2: inc i (z \cap (domain Y)) by rewrite zi; fprops. move: (fz i) => [_ fa]; move: (fa ii2) => fv; apply: (auxy _ _ idx fv). move=> [i [j [ltij zi]]]; move: (tcp1 _ _ ltij) => [idx jdy mt]. have ii2: inc j (z \cap (domain Y)) by rewrite zi; fprops. move: (fz j) => [_ fa]; move: (fa ii2) => fv; apply: (auxy _ _ jdy fv). exists B; split => // i idx. have : inc i (union C) by rewrite pca sR /E46_u; fprops. move=> /setU_P [y iy yC]; move: (fp1 _ yC i) => [fa _]. move: (fa (setI2_i iy idx)) => pc. exists (f y); apply /setI2_P;split => //; apply /funI_P; ex_tac. have : inc i (union C) by rewrite pca sR /E46_u; fprops. move=> /setU_P [y iy yC]; move: (fp1 _ yC i) => [_ fa]. move: (fa (setI2_i iy idx)) => pc. exists (f y); apply /setI2_P;split => //; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)