proposition: Lemma chordless_perimeter x : x \in bc -> edge x \in bc -> (x \in ac) || (edge x \in ac).
proof: Proof. have EercF: fband erc =i fband rc. move=> y; rewrite -Drrrc fband_rev_ring //. by apply: eq_has_r => z; rewrite mem_rev. move=> bc_x bc_ex; have [cycRerc /simple_uniq Uerc] := andP URerc. rewrite -negb_and; apply/andP=> [] [rcFx rcFex]. have erc_ok: proper_ring erc. move: rcFx cycRerc (edge_perimeter (head x rc)). case: (rc) => [|x1 [|x2 []]] //= _; first by rewrite /rlink cfaceC bridge'Gc. by rewrite !inE eqxx (inj_eq edgeI) => _ /norP[_]. move: x bc_x bc_ex rcFx rcFex. have rrc_ok: proper_ring rrc by rewrite -(proper_rev_ring geoGc) Drrrc. have nt_dFerc x: x \in fband erc -> edge x \in fband erc -> x \in diskE erc -> exists y, y \in diskF (chord_ring erc x). - move=> ercFx ercFex dEx; set rx := chord_ring erc x. have URrx: scycle rlink rx by apply: scycle_chord_ring. have rx_ok: proper_ring rx by apply: proper_chord_ring. have rx_erc: {subset behead rx <= erc}. have [[erc_jx xFj] [erc_jex exFj]] := (fprojP ercFx, fprojP ercFex). have [|i p1 _ Dp1 ->] := rot_to_arc Uerc erc_jex erc_jx. apply: contraTneq exFj => ->; rewrite cfaceC -(same_cface xFj). by rewrite bridge'Gc. rewrite -cat_cons {p1}Dp1 => Derc y rx_y. by rewrite -(mem_rot i) Derc mem_cat rx_y. have{ercFx ercFex dEx} dN_bc: {subset diskN rx <= bc}. move=> y; rewrite diskN_chord_ring // => /andP[_ /=]. by rewrite -Drrrc diskN_rev_ring ?inE //= diskN_E inE /= mem_rev => /norP[]. move: URrx rx_ok rx_erc dN_bc. elim: {x rx}_.+1 {-2}rx (ltnSn (size rx)) => // n IHn p; rewrite ltnS => lepn. move=> URp p_ok p_erc dN_bc; apply/existsP/pred0P => dF_0. have [cycRp /simple_uniq Up] := andP URp. case Dp: p (p_ok) => [|x p1] // _. have px: x \in p by rewrite Dp mem_head. have dNx: x \in diskN p by rewrite diskN_E !inE px. have bcx: x \in bc := dN_bc x dNx. have [[pF_F dN_N] dE_E] := (fbandF p, diskN_node p, diskE_edge planarGc URp). pose efex := edge (face (edge x)); pose enx := edge (node x). have f_efex: face efex = node x by rewrite /efex -{1}(n3c bcx) !nodeK. have [dEefex|] := boolP (efex \in diskE p). have pFefex: efex \in fband p. apply: contraFT (dF_0 (node x)); rewrite (fclosed1 pF_F) f_efex /=. by rewrite inE /= -(fclosed1 dN_N) => ->. have pFeefex: edge efex \in fband p. apply/hasP; exists (next p x); first by rewrite mem_next. by rewrite e2c -cface1; apply: next_cycle cycRp px. pose y := fproj p efex. have p1y: y \in p1. have [] := fprojP pFefex; rewrite -/y Dp inE => /predU1P[] // ->. by rewrite -{1}[x]nodeK -cface1r cface1 f_efex bridge'Gc. case/splitPr Dp1: p1 / p1y => [p2 p3]. have Dp2: efex :: p2 = chord_ring p efex. congr (_ :: _); rewrite -/y e2c /arc; set z := fproj p (face (edge x)). have ->: index z p = 1. have[]:= fprojP pFeefex; rewrite e2c -/z -cface1 cfaceC {2}Dp /= => pz. case: eqP => [<- | _ zFex]; first by rewrite bridge'Gc. move: cycRp; rewrite Dp; case: (p1) Dp => [|z1 p5] //= Dp /andP[xRz1 _]. rewrite -[z1](scycle_cface URp pz) ?eqxx ?(same_cface zFex) //. by rewrite Dp !inE eqxx orbT. rewrite Dp rot1_cons Dp1 rcons_cat index_cat /= eqxx addn0. rewrite [y \in p2](contraTF _ Up) ?take_size_cat //. by rewrite Dp /= Dp1 cat_uniq /= => ->; rewrite !andbF. have{IHn} [|||z p2z|z|z] := IHn (efex :: p2). + by apply: leq_trans lepn; rewrite Dp Dp1 /= size_cat /= addnS leq_addr. + by rewrite Dp2; apply scycle_chord_ring. + by rewrite Dp2; apply proper_chord_ring. + by rewrite p_erc // Dp Dp1 /= mem_cat p2z. + by rewrite Dp2 diskN_chord_ring // => /andP[_]; apply: dN_bc. by rewrite Dp2 diskF_chord_ring // inE /= [X in _ && X]dF_0 andbF. rewrite -(fclosed1 dE_E) inE /= (fclosed1 dN_N) edgeK dNx andbT negbK => pfex. case: p1 => [|fex p2] in Dp; first by rewrite Dp in p_ok. have Dfex: fex = face (edge x). apply: (scycle_cface URp) => //; first by rewrite Dp !inE eqxx orbT. by have:= cycRp; rewrite Dp /= /rlink cface1 cfaceC => /andP[]. have pFenx: enx \in fband p. by rewrite (fclosed1 pF_F) nodeK; apply: subsetP (ring_fband _) _ px. have pFeenx: edge enx \in fband p. apply/hasP; exists (next p fex); first by rewrite mem_next Dfex. by rewrite e2c -f_efex -cface1 Dfex; apply: next_cycle cycRp pfex. have dEenx: enx \in diskE p. rewrite -(fclosed1 dE_E) inE /= -(fclosed1 dN_N) dNx andbT Dp /= inE. have [_ /negPf->/=] := cubicP cubicGc x bcx. have rc_efex: efex \in rc. by rewrite -(mem_map edgeI) e2c -Dfex p_erc // Dp mem_head. have: 2 < arity efex < 7. by rewrite -mem_iota !inE [_ || _](allP (embeddable_ring embedGc)). rewrite ltnNge andbC /arity => /andP[_]; apply: contra => pnx. rewrite (eq_card (fconnect_cycle _ (mem_head _ [:: node x]))) ?card_size //. have fnxFefex: cface (face (node x)) efex by rewrite -f_efex -!cface1. rewrite /= f_efex eqxx andbT; apply/eqP/(scycle_cface UNrc)=> //. by rewrite (fclosed1 rcN) -(mem_map edgeI) faceK p_erc ?Dp. have Dp2: enx :: p2 = chord_ring p enx. congr (_ :: _); apply/esym. have <-: x = fproj p enx. have [pj enxFj] := fprojP pFenx; apply: (scycle_cface URp) => //. by rewrite -{1}[x]nodeK -cface1. have: cface (node x) (head x p2). by move: cycRp; rewrite -f_efex -cface1 Dp /= headI Dfex => /and3P[]. case: p2 Dp => [|z p3] Dp /= => [|nxFz]. by rewrite -{2}[x]nodeK -cface1r bridge'Gc. have <-: z = fproj p (edge enx). have [pj] := fprojP pFeenx; rewrite {1}e2c (same_cface nxFz). by apply: (scycle_cface URp); rewrite // Dp !inE eqxx !orbT. by move: Up; rewrite Dp -(cat1s fex); apply: right_arc. have{IHn} [|||z /= p2z|z|z] := IHn (enx :: p2). - by apply: leq_trans lepn; rewrite Dp. - by rewrite Dp2; apply: scycle_chord_ring. - by rewrite Dp2; apply: proper_chord_ring. - by rewrite p_erc // Dp mem_behead. - by rewrite Dp2 diskN_chord_ring // => /andP[_ /dN_bc]. by rewrite Dp2 diskF_chord_ring // inE /= [X in _ && X]dF_0 andbF. have dFerc_ac x: x \in fband erc -> edge x \in fband erc -> x \in diskE erc -> diskF (chord_ring erc x) =i ac. - move=> ercFx ercFex dEx; set rx := chord_ring erc x. have dF_ac: {subset diskF rx <= ac}. by move=> y; rewrite diskF_chord_ring // !inE EercF => /and3P[]. have URrx: scycle rlink rx by apply: scycle_chord_ring. have dN_dF: {in ac, {subset diskN rx <= diskF rx}}. move=> y; rewrite !inE /= -EercF. by rewrite -(fband_chord_ring _ _ ercFx) // -/rx => /norP[-> _]. move=> z; apply/idP/idP=> [|ac_z]; first exact: dF_ac. have [y dFy] := nt_dFerc x ercFx ercFex dEx; rewrite -/rx in dFy. have ac_eey: edge (edge y) \in ac by rewrite e2c dF_ac. have [p [eyRp Lp nt_p] [_ p_hac]] := h_spoke ac_eey ac_z. have{p_hac}: all (mem ac) p by move: p_hac; rewrite all_predI => /andP[]. case: p nt_p Lp eyRp => //= [y1 p] _ Lp /andP[eyRy1 y1Rp] /andP[_]. have{eyRy1} dFy1: y1 \in diskF rx. by rewrite -(closed_connect (diskF_face rx) eyRy1) e2c. rewrite -{Lp}(closed_connect (diskF_face rx) Lp). elim: p y1 dFy1 y1Rp => //= y2 p IHp y1 dFy1 /andP[y1Ry2 y2Rp] /andP[ac_y2]. apply: {p}IHp y2Rp; rewrite /rlink cface1 in y1Ry2. rewrite -(closed_connect (diskF_face rx) y1Ry2) dN_dF //. by rewrite inE /= (closed_connect (fbandF rc) y1Ry2). by rewrite (fclosed1 (diskN_node rx)) edgeK; case/andP: dFy1. move=> x bc_x bc_ex; rewrite /= -!EercF => ercFx ercFex. have dEex: edge x \in diskE erc. rewrite inE /= (mem_map edgeI) [~~ _]bc_x -Drrrc diskN_rev_ring //= !inE. apply: contra bc_ex => /hasP[y rrc_y /connectP[]]. rewrite mem_rev -{1}(f_finv nodeI y) -(fclosed1 rcN) in rrc_y. by case=> [|z p] => [_ -> | ] //=; rewrite {1}/dlink /= mem_rev rrc_y. have [||y dFy] := nt_dFerc _ ercFex; rewrite ?e2c //. have ac_y: y \in ac by rewrite dFerc_ac ?e2c in dFy. have /idPn[]:= dFy; rewrite diskF_chord_ring ?e2c // inE /= dFerc_ac ?ac_y //. by rewrite (fclosed1 (diskE_edge planarGc URerc)). 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)