proposition: Lemma embed_full : {in ac &, forall x1 x2, edge (h x1) = h x2 -> edge x1 = x2}.
proof: Proof. suffices IHf5: ~ exists x1, exists2 p, [/\ path rlink x1 p, last x1 p != x1 & {subset p <= ac}] & edge (h (last x1 p)) = h (edge x1) /\ size p <= 5. - move=> x1 x2 ac_x1 ac_x2 /= ehx1; apply/eqP/idPn=> x2'ex1; case: IHf5. have /radius2P[x0 ac_x0 ac_x0rad2] := embeddable_kernel embedGc. have /(at_radius2P acF)[x01 [x10 [x0Fx01 x1Fx10]]] := ac_x0rad2 x1 ac_x1. have /(at_radius2P acF)[x02 [x20 [x0Fx02 x2Fx20]]] := ac_x0rad2 x2 ac_x2. move=> [ac_ex02 ex02Fex20] [ac_ex01 ex01Fex10]. exists (edge x1), [:: x10; edge x01; x02; edge x20; x2]; last first. by split; rewrite //= e2c -ehx1 e2m. rewrite eq_sym; split=> //=. rewrite /rlink !e2c x1Fx10 cfaceC ex01Fex10 -(same_cface x0Fx01) x0Fx02. by rewrite ex02Fex20 cfaceC x2Fx20. apply/allP; rewrite /= ac_ex01 ac_x2 -(closed_connect acF x1Fx10) ac_x1. rewrite -(closed_connect acF x0Fx02) ac_x0. by rewrite -(closed_connect acF ex02Fex20) ac_ex02. suffices IHf5: ~ exists x, exists2 p, pre_hom_ring x p /\ ~~ rlink (last x p) x & size p <= 4. - move=> [x0 [p [x0Rp Lp p_ac] [Lhp ple5]]]. suffices{Lp Lhp}: exists2 q, [/\ path rlink x0 q, last x0 q = last x0 p & {subset q <= ac}] & simple (map h q) /\ size q <= size p. + case=> [[|x q] [x0Rq Lq q_ac] [Uq leqp]]. by rewrite -Lq /= eqxx in Lp. case: IHf5; exists x, q; last exact: leq_trans leqp ple5. have ac_x: x \in ac by rewrite q_ac ?mem_head. have{x0Rq Lq} /=[/andP[x0Rx xRq] Lq] := (x0Rq, Lq); split. apply: intro_pre_hom_ring; rewrite // Lq /rlink Lhp cfaceC. by rewrite cface_ac_h // cfaceC. apply: contra Lp => qRx0; apply/eqP/edgeI. have ac_eLp: edge (last x0 p) \in ac. by rewrite -Lq (closed_connect acF qRx0). apply: cface_inj_embed => //. by rewrite -Lq (same_cface qRx0) cfaceC. by rewrite embed_functor // -Lq q_ac ?mem_last. elim: p x0 x0Rp p_ac ple5 => [|x1 p IHp] x0 /=; first by exists [::]. case/andP=> [x0Rx1 x1Rp] /allP/=/andP[ac_x1 /allP p_ac] ple5. have{IHp x1Rp} [q [x1Rq Lq q_ac] [Uq leqp]] := IHp _ x1Rp p_ac (ltnW ple5). have [| qF'x1] := boolP (h x1 \in fband (map h q)); last first. exists (x1 :: q); split=> //; first by rewrite /= x0Rx1. by apply/allP; rewrite /= ac_x1; apply/allP. by rewrite map_cons simple_cons qF'x1. rewrite unfold_in has_map => /hasP[x2 q_x2]; rewrite /= cfaceC => hx2Fx1. have ac_x2: x2 \in ac := q_ac _ q_x2. have [x3 x2Fx3 eq_hx13] := cface_h_ac ac_x2 hx2Fx1. have ac_x3: x3 \in ac by rewrite -(closed_connect acF x2Fx3). case/splitP: {q}q_x2 x1Rq Lq leqp Uq q_ac => [q1 q2]. rewrite cat_path last_cat last_rcons cat_rcons size_cat /=. case/andP=> x1Rq1 x2Rq2 Lq2 leqp Uq q_ac. have [eq_x13 | x3'1] := eqVneq x1 x3. exists (x2 :: q2); split=> //. + by rewrite /= {1}/rlink (same_cface x0Rx1) eq_x13 cfaceC x2Fx3. + by move=> z q2z; rewrite q_ac // mem_cat q2z orbT. + by move: Uq; rewrite map_cat simple_cat => /and3P[_ _]. by rewrite (leqW (leq_trans _ leqp)) ?leq_addl. case: q1 => [|x q] in leqp Uq q_ac x1Rq1. have [x1Rx2 _] := andP x1Rq1. have ac_ex1: edge x1 \in ac by rewrite (closed_connect acF x1Rx2). have:= cface_ac_h ac_ex1 x1Rx2. by rewrite cfaceC embed_functor // (same_cface hx2Fx1) bridge'Gm. case: IHf5; exists x, (rcons q x3); last first. by rewrite size_rcons (leq_trans _ (leq_trans leqp ple5)) ?leq_addr. have ac_x: x \in ac := q_ac x (mem_head _ _). move: x1Rq1; rewrite /= rcons_path => /andP[x1Rx xRq]. have ac_ex1: edge x1 \in ac by rewrite (closed_connect acF x1Rx). rewrite last_rcons; split; last first. apply: contra x3'1; rewrite -(rlinkFr x1Rx) /rlink cfaceC => ex3Rex1. apply/eqP/edgeI/(cface_inj_embed ac_ex1 ex3Rex1). by rewrite !embed_functor ?eq_hx13 // -(closed_connect acF ex3Rex1). apply: intro_pre_hom_ring => //. + by rewrite rcons_path -(rlinkFr x2Fx3). + by rewrite last_rcons eq_hx13 /rlink -embed_functor // cface_ac_h. + move=> y; rewrite -rcons_cons mem_rcons inE => /predU1P[-> // | qy]. by rewrite q_ac // mem_cat qy. move: Uq; rewrite -rcons_cons -cat_rcons map_cat simple_cat !map_rcons. rewrite -!rot1_cons !simple_rot 2!simple_cons andbC => /andP[_]. by congr (_ && _); rewrite (closed_connect (fbandF _) hx2Fx1) eq_hx13. suffices IHf5: ~ exists x, exists2 p, pre_hom_ring x p /\ ~~ rlink (last x p) x & fcard face (diskF (map h (x :: p))) <= (size (x :: p) == 5). - case=> x [p xHRp lep5]; set xp := x :: p. have hp_ok: proper_ring (map h xp). rewrite {}/xp; case: p xHRp {lep5} => [|y [|y1 p1]] //= [] []. by rewrite /scycle /= /rlink cfaceC bridge'Gm. case/andP=> xRy _ /allP/=/and3P[ac_x ac_y _] _; apply: contraNneq => ehx. have ac_ex: edge x \in ac by rewrite (closed_connect acF xRy). rewrite -embed_functor // in ehx. by rewrite -(cface_inj_embed ac_ex xRy ehx) /rlink e2c. case: (IHf5); exists x, p => //. rewrite /= -(size_map h) eqSS leqNgt; apply/negP => nt_dF. have{xHRp} [[xRp p_ac URhp] Lp] := xHRp. have hxFehp: cface (h x) (edge (h (last x p))). by have[] := andP URhp; rewrite /= rcons_path last_map cfaceC => /andP[]. have ac_x: x \in ac := p_ac x (mem_head x _). case/lastP Dp: p => [|p1 y]; first by rewrite Dp /= bridge'Gm in hxFehp. have Dy: y = last x p by rewrite Dp last_rcons. have ac_y: y \in ac by rewrite Dy p_ac ?mem_last. have [ry xFry hry] := cface_h_ac ac_x hxFehp. pose rp := rcons (rev (map edge (belast x p1))) ry. pose rx := edge (last x p1); pose rxp := rx :: rp. have Ehrp: map h rxp = rot 1 (rev_ring (map h xp)). rewrite /xp lastI /rev_ring !map_rcons rev_rcons rot1_cons -hry. rewrite Dp belast_rcons {}/rxp {}/rx {}/rp -rcons_cons. rewrite -rev_rcons -map_rcons -lastI map_rcons map_rev -!map_comp. congr (rcons (rev _) _); apply/eq_in_map => z pz. move/allP: p_ac xRp; rewrite {}Dp; case/splitPl: pz => p2 p3 Lp2. rewrite rcons_cat -cat_cons cat_path headI lastI Lp2 cat_rcons all_cat. set z1 := head y p3 => /and4P[_ ac_z ac_z1 _] /and3P[_ zRz1 _]. by rewrite /= embed_functor // (closed_connect acF zRz1). case: IHf5; exists rx, rp. split; last first. move: xRp; rewrite Dp rcons_path => /andP[_ p1Ry]. rewrite last_rcons (rlinkFr p1Ry); apply: contra Lp => ryRy. have ac_ry: ry \in ac by rewrite -(closed_connect acF xFry). have ac_ery: edge ry \in ac by rewrite (closed_connect acF ryRy). have:= canLR e2m hry; rewrite -Dy -embed_functor // => Dhy. by rewrite -(cface_inj_embed _ _ Dhy) // /rlink e2c cfaceC. split=> [|z|]; last 1 first. + by rewrite Ehrp rot_scycle; apply: scycle_rev_ring. + move: xFry xRp; rewrite cfaceC {rxp Ehrp}/rx {}/rp {hry}Dp. elim: p1 ry (x) => [|x3 p1 IHp] x1 x2 /= x1Fx2 /andP[x2Rx3 x3Rp]. by rewrite /rlink e2c cfaceC x1Fx2. by rewrite rev_cons rcons_path last_rcons IHp // /rlink e2c cfaceC. rewrite -rcons_cons mem_rcons -rev_rcons inE /= mem_rev -map_rcons -lastI. rewrite -{2}[z]e2c (mem_map edgeI) => /predU1P[->|p1ez]. by rewrite -(closed_connect acF xFry). move/allP: p_ac xRp; rewrite {}Dp; case/splitPl: p1ez => [p2 p3 Lp2]. rewrite rcons_cat cat_path Lp2 headI /= all_cat /= /rlink e2c. by case/and4P=> _ _ ac_x3 _ /and3P[_ /(closed_connect acF)-> _]. have EhrpF: diskF (map h rxp) =i diskF (rev_ring (map h xp)). by move=> z; rewrite Ehrp diskF_rot. have <-: size (map h xp) = size rxp. by rewrite size_map /= Dp !size_rcons size_rev size_map size_belast. rewrite (eq_n_comp_r EhrpF) (eq_n_comp_r (diskF_rev_ring cexGm URhp hp_ok)). apply: contraFT (Birkhoff cexGm _ URhp); last by rewrite size_map. by rewrite -ltnNge => nt_dFC; apply/andP. case=> x [p [xHRp Lp] triv_dF]; have [] := negP Lp. apply: trivial_hom_ring => //. do [move Dxp: (x :: p) => xp; case: eqP => // sz_xp_5] in triv_dF *. set hxp := map h xp; rewrite leqn0; apply/exists_inP=> [[u /= Du dFu]]. have{xHRp} [xRp p_ac URhxp] := xHRp; rewrite Dxp -/hxp in p_ac URhxp. have{Du dFu triv_dF} DdF v: (v \in diskF hxp) = cface u v. have dFcF := closed_connect (diskF_face hxp). apply/idP/idP=> [dFv | /dFcF <- //]; apply/(rootP cfaceC)/esym/eqP. move: triv_dF; rewrite [fcard _ _](cardD1 u) inE /= Du dFu ltnS leqn0. move/pred0P/(_ (froot face v)); rewrite /= inE /= (roots_root cfaceC) /=. by rewrite -(dFcF _ _ (connect_root _ _)) (eqP Du) dFv andbT => /negbFE. pose ru := spoke_ring u; pose frf := froots (@face Gm). have{frf} DxpF: fband hxp =i fband ru. have ruF_xpF: [predI frf & fband ru] \subset [predI frf & fband hxp]. apply/subsetP=> v1 /andP/=[Dv1 /hasP[v ru_v v1Fv]]. rewrite inE /= (closed_connect (fbandF hxp) v1Fv) {v1 v1Fv}Dv1 /=. have{ru_v} uFnv: cface u (node v) by rewrite -mem_spoke_ring. have dNnv: node v \in diskN hxp by move: uFnv; rewrite -DdF => /andP[]. have: v \notin diskF hxp. by rewrite DdF (same_cface uFnv) -{2}[v]nodeK -cface1r bridge'Gm. by rewrite inE /=; apply: contraR => ->; rewrite (fclosed1 (diskN_node _)). have EpFr: fcard face (fband ru) = fcard face (fband hxp). apply/eqP; rewrite eqn_leq subset_leq_card //. rewrite (scycle_fcard_fband URhxp) size_map sz_xp_5. rewrite (@scycle_fcard_fband Gm rlink); last exact: scycle_spoke_ring. by rewrite size_spoke_ring pentaGm. move=> v; have:= subset_cardP EpFr ruF_xpF (froot face v). rewrite !inE (roots_root cfaceC) /=. by rewrite -!(closed_connect (fbandF _) (connect_root _ v)). have hxp_ru: {subset hxp <= ru}. move=> v hxp_v; have [cycRhxp _] := andP URhxp. have uAv: adj u v. by rewrite -fband_spoke_ring -DxpF (subsetP (ring_fband _)). have uAev: adj u (edge v). rewrite (adjFr (next_cycle cycRhxp hxp_v)) -fband_spoke_ring -DxpF. by rewrite (subsetP (ring_fband _)) ?mem_next. have /orP[//|] := adj11_edge cexGm uAv uAev. rewrite mem_spoke_ring -DdF => /andP[_] /=. rewrite -(fclosed1 (diskN_node _)) diskN_edge_ring //. by rewrite /hxp -(mkseq_nth x xp) sz_xp_5. have: fcycle (face \o face \o edge) hxp. have [[cycRhxp UhxpF] URu] := (andP URhxp, scycle_spoke_ring cexGm u). apply cycle_from_next=> [|v hxp_v]; first exact: simple_uniq. apply/eqP/(scycle_cface URu); first 2 [by rewrite hxp_ru ?mem_next]. by rewrite /= -(next_spoke_ring cexGm (hxp_ru v hxp_v)) mem_next hxp_ru. by rewrite -!cface1; apply: next_cycle cycRhxp hxp_v. rewrite /hxp -Dxp /= rcons_path last_map => /andP/=[hxFFEhp /eqP Lhp]. have nxp_nxF: map node xp \subset cface (node x). rewrite subset_all -Dxp /= inE connect0 /=. move/allP: p_ac xRp hxFFEhp; rewrite -Dxp /=. elim: (p) (x) => //= x2 r IHr x1 => /andP[ac_x1 r_ac] /andP[x1Rx2 x2Rp]. case/andP=> /eqP/esym Dhx2 hx2FFEhr; have [ac_x2 _] := andP r_ac. suffices{r IHr r_ac x2Rp hx2FFEhr} nx1Fnx2: cface (node x1) (node x2). by rewrite inE nx1Fnx2 (eq_all (same_cface nx1Fnx2)) IHr. have ac_ex1: edge x1 \in ac by rewrite (closed_connect acF x1Rx2). rewrite -embed_functor // -!hF -?(fclosed1 acF) // in Dhx2. have: cface x2 (face (face (edge x1))) by rewrite cfaceC -!cface1. move/cface_inj_embed->; rewrite // -(canRL edgeK (e2c _)) cface1r. by rewrite -{2}(n3c (ac_bc ac_x1)) !nodeK. have ac'nx: (node x \notin ac). apply: contra Lp => ac_nx; set y := last x p in Lhp *; rewrite -Dxp in p_ac. have ac_x: x \in ac := p_ac x (mem_head x p). have ac_enx: edge (node x) \in ac by rewrite (fclosed1 acF) nodeK. have ac_y: y \in ac := p_ac y (mem_last x p). have ac_eny: edge (node y) \in ac by rewrite (fclosed1 acF) nodeK. have nxFny: cface (node x) (node y). by apply: (subsetP nxp_nxF); rewrite map_f // -Dxp mem_last. have ac_ny: node y \in ac by rewrite -(closed_connect acF nxFny). have hny: h (node y) = h (face (node x)). rewrite hF // -[h (node x)]edgeK -embed_functor // -hF // nodeK -Lhp. rewrite -[h y]n3m -(canRL edgeK (e2m _)) !nodeK. by rewrite -{2}[y]nodeK hF // embed_functor // edgeK. have nyFfnx: cface (node y) (face (node x)) by rewrite cfaceC -cface1. have bc_y: y \in bc := ac_bc ac_y. rewrite /rlink -(n3c bc_y) 2!cface1 nodeK -[node (node y)]e2c. by rewrite (cface_inj_embed ac_ny nyFfnx) // faceK nodeK. have nxp_ace: map node xp \subset [predI cface (node x) & [preim edge of ac]]. apply/subsetP=> y nxp_y; rewrite inE /= (subsetP nxp_nxF) //= inE /=. by have{y nxp_y} [z xp_z ->] := mapP nxp_y; rewrite (fclosed1 acF) nodeK p_ac. have:= leq_trans (subset_leq_card nxp_ace) (adj_kernel_max ac'nx). suffices /card_uniqP->: uniq (map node xp) by rewrite size_map sz_xp_5. by rewrite (map_inj_uniq nodeI); have [_ /simple_uniq/map_uniq] := andP URhxp. 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)