proposition: Lemma embed_functor x : x \in ac -> edge x \in ac -> h (edge x) = edge (h x).
proof: Proof. suffices{x}: ~ exists2 x, x \in [predD ac & hc] & exists2 p, scycle rlink (x :: p) & {subset p <= [predI ac & hc]}. - move=> IH ac_x ac_ex; apply/eqP/idPn=> eh'hex; case: IH. exists x => [|{eh'hex}]; first by rewrite !inE eh'hex. case: {ac_ex ac_x}(h_spoke ac_ex ac_x) => p []; case/lastP: p => // p y xRp. rewrite last_rcons all_rcons => yFx _ [Up /andP[_ /allP ac_p]]. exists p => //; rewrite /scycle /= rcons_path -(rlinkFr yFx) -rcons_path xRp. by rewrite simple_cons -(closed_connect (fbandF p) yFx) -simple_rcons. suffices: ~ exists2 x, x \notin hc & exists2 p, scycle rlink (x :: p) & {subset p <= hc} /\ {subset diskN (x :: p) <= ac}. - move=> IH [x /andP[/= eh'hex ac_x] [p URp hac_p]]. have ac_xp: {subset (x :: p) <= ac} by move=> y /predU1P[-> | /hac_p/andP[]]. have [dF'rc|] := boolP (all [predC diskF (x :: p)] rc). case: IH; exists x => //; exists p => //. split=> [y | y dNy]; first by case/hac_p/andP. case xpFy: (y \in fband (x :: p)). case/(@hasP _ _ (x :: p)): xpFy => z pz yFz. by rewrite (closed_connect acF yFz) ac_xp. apply: contraL dF'rc => /hasP[z rc_z yFz]. rewrite all_predC negbK; apply/hasP; exists z => //=. by rewrite -(closed_connect (diskF_face _) yFz) !inE xpFy. have rr_xp1: rev_ring (rot 1 (x :: p)) = edge x :: rev_ring p. by rewrite {1}/rev_ring map_rot /= rot1_cons rev_rcons. have URp1: scycle rlink (rot 1 (x :: p)) by rewrite rot_scycle. rewrite all_predC negbK => /= dF'rc. case: IH; exists (edge x); first by rewrite hcE. exists (rev_ring p); first by rewrite -rr_xp1; apply: scycle_rev_ring. split=> y; first by rewrite -hcE /= mem_rev_ring // => /hac_p/andP[]. have proper_xp1: proper_ring (rot 1 (x :: p)). rewrite proper_ring_rot //; case: (p) URp hac_p => [|x2 []] //=. by rewrite /scycle /= /rlink cfaceC bridge'Gc. move=> _ /allP/=/andP[/andP[_ hcx2] _]; apply: contraTneq hcx2 => <-. by rewrite /= hcE. rewrite /= -rr_xp1 diskN_rev_ring // inE => /= dNr'y. apply/hasP => [] [z rcz yFz]. have: z \in diskF (x :: p). apply/andP; split. apply/hasP=> [] [t rct tFz]; case/ac_xp/hasP: rct. by exists z; rewrite // cfaceC. case/hasP: dF'rc => t; rewrite -(fconnect_cycle cycNrc rcz) => zNt /=. by rewrite (closed_connect (diskN_node _) zNt) => /andP[]. rewrite -(closed_connect (diskF_face _) yFz) => /andP[_]. rewrite /= unfold_in => /hasP[y1 xpy1 yDy1]. case/hasP: dNr'y; exists y1; first by rewrite mem_rot. apply: etrans yDy1; apply: {y1 xpy1}eq_connect => y1 y2. by rewrite /dlink /= mem_rot. case=> x hc'x [p URp []]; move: {2}_.+1 (ltnSn #|diskN (x :: p)|) URp => n. elim: n => // n IHn in x hc'x p *; rewrite ltnS => le_dN_n URp p_hc dN_ac. set xp := x :: p in le_dN_n URp p_hc dN_ac. have dNx: x \in diskN xp by rewrite diskN_E mem_head. have dNnx: node x \in diskN xp by rewrite -(fclosed1 (diskN_node xp)). have dNnnx: node (node x) \in diskN xp by rewrite -(fclosed1 (diskN_node xp)). have [cycRp UpF] := andP URp; have Up := simple_uniq UpF; rewrite /xp in cycRp. case Dp0: p (cycRp) => [|x0 p0]; first by rewrite /= /rlink cfaceC bridge'Gc. clear 1; pose enx := edge (node x); pose p1 := rcons p enx. have xRp1: path rlink x p1. by rewrite rcons_path /= {2}/rlink cface1r /enx nodeK -rcons_path. have{UpF} Up1: simple p1. have enxFx: cface enx x by rewrite cface1 nodeK. by rewrite /p1 simple_rcons (closed_connect (fbandF p) enxFx) -simple_cons. have [n3x x'nx] := cubicP cubicGc _ (ac_bc (dN_ac x dNx)). case hc_nx: (node x \in hc). case hc_nnx: (node (node x) \in hc). case/eqP: hc'x; apply: faceI; rewrite -(canRL nodeK (n3m _)). do 2!apply: (canRL (canF_sym nodeK)); rewrite -{1}n3x -hF; last first. by rewrite inE /= (fclosed1 (fbandF rc)) nodeK [~~ _]dN_ac. rewrite nodeK -(eqP hc_nnx) -hF; last first. by rewrite inE /= (fclosed1 (fbandF rc)) nodeK [~~ _]dN_ac. rewrite nodeK -(eqP hc_nx) -hF ?nodeK //. by rewrite inE /= (fclosed1 (fbandF rc)) nodeK [~~ _]dN_ac. pose ennx := edge (node (node x)). pose i := find (cface ennx) p1; pose q := ennx :: take i p1. have le_i_p1: i <= size p1 by apply: find_size. have URq: scycle rlink q. have{xRp1} ennxRp1: path rlink ennx p1. move: xRp1; rewrite -(drop0 p1) (drop_nth x) ?nth0 ?size_rcons //=. by rewrite {3}/rlink /= e2c (canRL nodeK n3x) -cface1. apply/andP; move: le_i_p1 ennxRp1 Up1; rewrite leq_eqVlt. case/predU1P=> [eq_i_p1 | lt_i_p1]. rewrite /q eq_i_p1 take_size /= rcons_path simple_cons => -> ->. rewrite last_rcons /rlink /= cface1r nodeK e2c [_ \in _]has_find -/i. by rewrite eq_i_p1 ltnn. rewrite -(cat_take_drop i.+1 p1) (take_nth x) //= cat_path last_rcons. have ennxFi: cface ennx (nth x p1 i) by apply: nth_find; rewrite has_find. rewrite !rcons_path -(rlinkFr ennxFi) simple_cat => /andP[-> _] /andP[]. rewrite -rot1_cons simple_rot !simple_cons. by rewrite -(closed_connect (fbandF _) ennxFi). have p1_hc: {subset take i p1 <= hc}. move=> y /mem_take; rewrite mem_rcons => /predU1P[-> | /p_hc//]. by rewrite hcE. have dNq'x: (x \in diskN q) = false. rewrite 2!(fclosed1 (diskN_node q)) -[node _]e2c. apply: (diskN_edge_ring geoGc URq _ (mem_head _ _)). rewrite /q; case Dp2: (take i p1) => [|x1 [|x2 p2]] //. by rewrite /scycle /q Dp2 /= /rlink cfaceC bridge'Gc in URq. apply: contraFN hc_nnx; rewrite e2c => /eqP->. by rewrite p1_hc //= Dp2 ?mem_head. suffices dNq_dN: {subset diskN q <= diskN xp}. have{hc_nnx} hc'ennx: ennx \notin hc by rewrite hcE hc_nnx. case: {IHn}(IHn _ hc'ennx (take i p1)) => // [|_ /dNq_dN/dN_ac//]. apply: leq_trans le_dN_n; rewrite -/q [rhs in _ < rhs](cardD1 x) dNx ltnS. apply/subset_leq_card/subsetP=> y dNq_y; rewrite !inE dNq_dN // andbT. by apply: contraFN dNq'x => /eqP <-. move=> t; rewrite unfold_in => /hasP[z q_z /connectP[r yDr ->{t}]]. move: yDr; set y := finv node z. have: y \in diskN xp /\ y \in diskN q. rewrite !(fclosed1 (diskN_node _) y)(f_finv nodeI) !diskN_E /=. rewrite [diskE]lock [q]lock !inE -!lock q_z -orbA; split=> //=. have [_|p'z /=] := boolP (z \in p); first exact: orbT. move: q_z; rewrite inE /p1 -cats1 take_cat // 2!fun_if mem_cat. case/predU1P=> [-> | ]. rewrite -(fclosed1 (diskE_edge planarGc URp)) inE /= dNnnx orbC. rewrite (contraFN _ hc_nnx) // inE -(inj_eq nodeI) n3x. by rewrite eq_sym (negPf x'nx) => /p_hc. rewrite (contraNF (@mem_take i _ p z) p'z) (negPf p'z). rewrite ltn_neqAle; case: eqP => [-> | _ /=]; first by rewrite subnn. rewrite -ltnS -(size_rcons p enx) -has_find; case: ifPn => // p1F'ennx. case: (i - _) => //= _; rewrite inE => /eqP Dz. rewrite Dz -(fclosed1 (diskE_edge planarGc URp)) inE orbC /= dNnx. rewrite inE (negPf x'nx) (contra _ p1F'ennx) // => pnx. apply/hasP; exists (node x); first by rewrite mem_rcons mem_behead. by rewrite cface1 nodeK. elim: {z q_z}r y => [|z r IHr] y [dNy dNq_y] //=. rewrite {1}/dlink /= -andbA => /and3P[q'y yCz]; apply: {r}IHr. rewrite !(fclosed1 (diskN_node _) z). have{z yCz} [<- // | <-] := clinkP yCz. rewrite !diskN_E !(fclosed1 (diskE_edge _ _) (node _)) // !faceK. rewrite ![y \in diskE _]inE /= q'y {}dNy dNq_y orbT andbT; split=> //. apply/orP; right; rewrite inE; case: eqP (dNq'x) => [<- /idP// | _ _] /=. apply: contra q'y => py; rewrite !inE -[p1]cats1 take_cat orbC {le_i_p1}. case: ifP => lt_i_p; last by rewrite mem_cat py. without loss{py}: / y \in drop i p. by move: py; rewrite -{1}(cat_take_drop i p) mem_cat => /orP[] -> // ->. rewrite (drop_nth x) // => p_y; case/idP: dNq'x. move: (mem_rot 1 xp) cycRp Up; rewrite -(rot_uniq 1) rot1_cons /=. rewrite -(cat_take_drop i.+1 p) rcons_cat. case/splitPl: p_y => r0 r Lr0; rewrite rcons_cat cat_uniq catA. rewrite -[x in x \in _](last_rcons y r); move: {r}(rcons r x) => r. rewrite has_cat cat_path last_cat (take_nth x) // last_rcons {}Lr0. move=> Dxp /andP[_ yRr] /and3P[_ /norP[_ Ur] _]. have{r0 Dxp Ur}: ~~ has (mem (fband q)) r. apply: contra Ur => /hasP[z rz /= qFz]; apply/hasP; exists z => //=. have /hasP[t p_t zFt]: z \in fband (rcons (take i p) (nth x p i)). move: qFz; rewrite -rot1_cons fband_rot !fband_cons -[p1]cats1 take_cat. rewrite lt_i_p; congr (_ || _); apply: (same_connect_r cfaceC). suffices: cface ennx (nth x p1 i) by rewrite nth_rcons lt_i_p. by apply: nth_find; rewrite has_find size_rcons leqW. by rewrite (scycle_cface URp _ _ zFt) // -Dxp !mem_cat (p_t, rz) ?orbT. elim: r y dNq_y yRr => //= z r IHr y dNq_y /andP[yRz rRr] /norP[qF'z qF'r]. suffices: z \in diskF q by case/andP=> _ /IHr->. rewrite /rlink cface1 in yRz; rewrite -(closed_connect (diskF_face q) yRz). rewrite inE /= (closed_connect (fbandF q) yRz) qF'z. by rewrite (fclosed1 (diskN_node q)) edgeK. have dNenx: enx \in diskN xp. rewrite diskN_E inE orbC /= -(fclosed1 (diskE_edge _ _)) // inE /= dNnx. by rewrite (contraFN _ hc_nx) // inE (negPf x'nx); apply: p_hc. have ac_eenx: edge enx \in ac by rewrite e2c dN_ac. have [q1 [enxRq1 Lq1 ntq1] [Uq1 q1_ac]] := h_spoke ac_eenx (dN_ac _ dNenx). pose i := find (mem (fband p1)) q1; pose q2 := take i q1. have Upq2: ~~ has (mem (fband q2)) p1. apply/hasP=> [] [y p1y] /(has_nthP x)[j]. rewrite size_take leq_min => /andP[ltji _]; rewrite nth_take // => yFq1j. by have /hasP[] := before_find x ltji; exists y; last by rewrite cfaceC. have p1Fq1: has (mem (fband p1)) q1. apply/hasP; exists (last enx q1). by case: (q1) ntq1 => //= nx' q11 _; apply: mem_last. by apply/hasP; exists enx; first by rewrite mem_rcons mem_head. have lt_i_q1: i < size q1 by rewrite -has_find. have /hasP[y p1y y1Fy] := nth_find x p1Fq1. move: (simple_uniq Up1) Upq2 (last_rcons y p enx) {Up}; rewrite -/p1. case/splitPr Dp: p1 / p1y => [p2 p3] Up. rewrite last_cat /= has_cat => /norP[Up2q Up3q] Lp3. pose q3 := q2 ++ belast y p3; pose q := enx :: q3. have{y1Fy} URq: scycle rlink q. apply/andP; split. rewrite /= -{2}Lp3 rcons_cat -lastI cat_path. rewrite -(cat_take_drop i q1) -/q2 (drop_nth x) // cat_path in enxRq1. case/and3P: enxRq1 => ->; rewrite (rlinkFr y1Fy) /= => -> _. by have:= xRp1; rewrite Dp cat_path /= => /and3P[]. rewrite -(simple_rot 1) rot1_cons rcons_cat -Lp3 -lastI simple_cat Up3q /=. have:= Uq1; rewrite -(cat_take_drop i q1) simple_cat => /andP[-> _]. by have:= Up1; rewrite Dp simple_cat => /and3P[]. have p3_p: {subset (belast y p3) <= p}. have ->: p = behead (belast x p1) by rewrite belast_rcons. rewrite Dp belast_cat /= -cat_rcons -lastI /=. by move=> z p3z; rewrite mem_cat p3z orbT. have q3_hc: {subset q3 <= hc}. move=> z; rewrite mem_cat => /orP[/mem_take q1z | /p3_p/p_hc//]. by have /andP[] := allP q1_ac z q1z. have dNq'x: (x \in diskN q) = false. rewrite (fclosed1 (diskN_node q)) -[node x]e2c -/enx. apply: diskN_edge_ring (mem_head _ _) => //. case/andP: URq (q3_hc (node x)); rewrite /q hc_nx. case: (q3) => [|y2 [_ _|]] //=; first by rewrite /rlink e2c bridge'Gc. by move/implyP; rewrite inE implybF e2c. suffices{IHn} dNq_dN: {subset diskN q <= diskN xp}. have{hc_nx} hc'enx: enx \notin hc by rewrite hcE hc_nx. case: {IHn}(IHn _ hc'enx q3) => // [|_ /dNq_dN/dN_ac//]. apply: leq_trans le_dN_n; rewrite -/q [rhs in _ < rhs](cardD1 x) dNx ltnS. apply/subset_leq_card/subsetP=> z dNq_z; rewrite !inE dNq_dN // andbT. by apply: contraFN dNq'x => /eqP <-. move=> z0 /(@hasP _ _ q)[z2 qz2 /connectP[r z1Dr ->]]; move: z1Dr. set z1 := finv node z2. have{qz2}: z1 \in diskN xp /\ z1 \in diskN q. rewrite !(fclosed1 (diskN_node _) z1) (f_finv nodeI). split; last by rewrite diskN_E qz2. move: qz2; rewrite -[q]cat_cons mem_cat => /orP[q2z2 | p3z2]; last first. by rewrite diskN_E !inE p3_p ?orbT. have Uq2p: ~~ has (mem (fband xp)) q2. have: ~~ has (mem (fband q2)) p1 by rewrite Dp has_cat negb_or Up2q. apply: contra => /hasP[t q2t /(@hasP _ _ xp)[u pu uFt]]. move: pu; rewrite inE => /predU1P[Du | pu]. apply/hasP; exists enx; first by rewrite mem_rcons mem_head. by apply/hasP; exists t; rewrite // cface1 nodeK -Du cfaceC. apply/hasP; exists u; first by rewrite mem_rcons mem_behead. by apply/hasP; exists t; last by rewrite cfaceC. case/andP: URq Uq2p; rewrite /q /= rcons_cat /q3. case/splitPl: q2z2 => q4 q5 <-; rewrite -catA cat_path has_cat. case/andP=> enxRq4 _ _ /norP[Uq4p _] {q5}. elim: q4 (enx) enxRq4 dNenx Uq4p => //= v q4 IHq u. rewrite {1}/rlink cface1 => /andP[fuRv vRq4] dNu /norP[xpF'x xpF'q4]. suffices: v \in diskF xp by case/andP=> _ /IHq->. rewrite -(closed_connect (diskF_face xp) fuRv) inE /=. rewrite (closed_connect (fbandF xp) fuRv) xpF'x. by rewrite (fclosed1 (diskN_node xp)) edgeK dNu. elim: r {z2}z1 => [|z2 r IHr] z1 [dNz1 dNq_z1] //= /andP[] /andP[q'z1 z1Cz2]. apply: {r}IHr; rewrite !(fclosed1 (diskN_node _) z2). case/clinkP: z1Cz2 => <- //; rewrite -(canRL edgeK (e2c _)). rewrite !diskN_E -!(fclosed1 (diskE_edge _ _)) // ![z1 \in diskE _]inE /=. rewrite {}dNz1 dNq_z1 q'z1 orbT andbT orbC; split=> //. have {1}->: xp = belast x p1 by rewrite belast_rcons. rewrite Dp belast_cat /= -cat_rcons -lastI {q'z1}(contra _ q'z1) //. rewrite -[q]cat_cons !mem_cat => /orP[xp2z1 | ->]; last exact: orbT. have Uqp2: ~~ has (mem (fband q)) p2. apply/hasP=> [] [t p2t /(@hasP _ _ q)[u qu tFu]]. have:= qu; rewrite -(mem_rot 1) rot1_cons rcons_cat -Lp3 -lastI mem_cat. case/orP=> [q2u | p3u]. by case/hasP: Up2q; exists t; last by apply/hasP; exists u. have:= Up1; rewrite Dp simple_cat => /and3P[_ /hasP[]]. by exists u; last by apply/hasP; exists t; rewrite 1?cfaceC. case/negP: dNq'x; have:= xRp1; rewrite Dp cat_path => /andP[xRp2 _]. case/splitPl: xp2z1 xRp2 Uqp2 dNq_z1 => p4 p5 <- {z1}. rewrite cat_path has_cat => /andP[xRp4 _] /norP[qF'p4 _] {p5}. elim/last_ind: p4 xRp4 qF'p4 => // r z IHr. rewrite last_rcons rcons_path has_rcons {2}/rlink /= cface1. case/andP=> xRp ferFz /norP[qF'z qF'r] dNq_z. have: z \in diskF q by apply/andP. rewrite -(closed_connect (diskF_face q) ferFz) => /andP[_] /=. by rewrite (fclosed1 (diskN_node q)) edgeK; apply: IHr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)