proposition: Lemma Euler_tree G (x : G) : Jordan G -> ~~ [disjoint cedge x & [pred y | clink y y || ~~ cross_edge y]].
proof: Proof. move: x => x0 JordanG; rewrite disjoint_subset; apply/subsetP=> tree_x0. have rfP := rootP (@cfaceC G); move: (froot face) => rf in rfP. have rfF x: rf (face x) = rf x by apply/rfP; rewrite -cface1. pose simple := [pred p | uniq (map rf p)]. have [x x0Ex [p1 [xEp1 Sp1 Lp1]]]: exists2 x, cedge x0 x & exists p1, [/\ fpath edge x p1, simple (x :: p1) & cface (last x p1) (node (face x))]. - have /connectP[p0 ex0Ep0 Lp0]: cedge (edge x0) x0 by rewrite cedgeC fconnect1. pose p := edge x0 :: p0; pose x := x0; rewrite (Lp0 : x0 = last x p). have{Lp0} notSp: ~~ simple (x :: p) by rewrite [x]Lp0 /= -last_map mem_last. have{ex0Ep0} xEp: fpath edge x p by rewrite /= eqxx. elim: {p0}p x xEp notSp => //= _ p IHp x /andP[/eqP<- exEp]. rewrite negb_and negbK -cons_uniq -map_cons orbC [~~ _ || _]if_neg. case: ifPn => [{IHp}Sp pFx | notSp _]; last exact: IHp notSp. exists (edge x); first by rewrite cedgeC; apply/connectP; exists p. case/mapP: pFx Sp exEp => y /splitPl[p1 p2 Lp1] /rfP-xFy. rewrite -cat_cons map_cat cat_uniq cat_path => /andP[Sp1 _] /andP[exEp1 _]. by exists p1; rewrite Lp1 edgeK cfaceC. do [set fx := face x; set nfx := node fx; set z1 := last x p1] in Lp1. have{x0 x0Ex tree_x0} tree_x := tree_x0 _ (connect_trans x0Ex _). have{Lp1} [q1 [fxCq1 Lq1 Uq1 _ z1Fq1]]: exists q1, let q := fx :: q1 in [/\ path clink fx q1, last fx q1 = nfx, uniq q, map rf q =i map rf (x :: p1) & forall y, face y \in q -> y \in belast z1 q]. - have spFC y p: fpath face y p -> path clink y p by apply/sub_path/subrelUr. move: nfx {tree_x} => z in Lp1 *. elim: p1 => /= [|y p IHp] in x z1 fx xEp1 Lp1 Sp1 *. have{Lp1} /connectP[_ /shortenP[q fxFq Uq _] Lq]: cface (face x) z. by rewrite -cface1. exists q; rewrite spFC //; split=> //= y. rewrite !inE -(rfF x) eq_sym orb_idr // => {y}/mapP[y q_y ->]. by rewrite (sameP eqP (rfP _ _)) (path_connect fxFq) //= mem_behead. rewrite !inE (inj_eq faceI); case: (y == x) => //= q_fy. case/splitPr: q_fy fxFq => q1 q2; rewrite cat_path => /and3P[_ /eqP-Dfy _]. by rewrite belast_cat -(faceI Dfy) mem_cat mem_head orbT. have{xEp1 Sp1} [[/eqP-Dy yEp] [p'Fx Sp]] := (andP xEp1, andP Sp1). have{IHp yEp Lp1 Sp} [q2 [fexCq2 Lq2 Uq2 rf_q2 z1Fq2]] := IHp y yEp Lp1 Sp. have /connectP[_ /shortenP[q1 fxFq1 Uq1 _] Lq1]: cface fx x by apply/rfP/rfF. have q1x: x \in fx :: q1 by rewrite Lq1 mem_last. have cFq1: fcycle face (fx :: q1) by rewrite (cycle_path x) /= -Lq1 eqxx. have{cFq1 q1x} q1Fx t: cface x t = (t \in fx :: q1) by apply: fconnect_cycle. exists (q1 ++ face y :: q2); rewrite cat_path -Lq1 last_cat spFC //=. split=> // [||t|t]; first by rewrite -[x]edgeK Dy clinkN. - rewrite -cons_uniq -cat_cons cat_uniq Uq1; case: hasP => //= -[t q2t q1t]. by rewrite (rfP x t _) ?q1Fx // -rf_q2 -map_cons map_f in p'Fx. - rewrite map_cat 2!inE mem_cat rf_q2 orbA rfF [lhs in lhs || _]orb_idr //. by case/mapP=> {}t q1t ->; rewrite (rfP x t _) ?q1Fx // mem_behead. rewrite belast_cat -cat_cons mem_cat -q1Fx /= -cat_rcons -lastI -cface1r. by rewrite [t \in _]inE mem_cat orbCA -q1Fx; case: (cface x t) => // /z1Fq2. have{rf rfP rfF simple Sp1} p1'fx: fx \notin x :: p1. apply: contra (tree_x x _); rewrite // !inE (sameP clinkP pred2P). by case/orP=> [-> | p1fx]; rewrite ?orbT //= -rfF map_f in Sp1 *. have xEnfx: cedge x nfx by rewrite cedge1r faceK. have xEfx: cedge x fx. suffices clNEx: fclosed node (cedge x) by rewrite [cedge _ _](fclosed1 clNEx). apply: (intro_closed cnodeC) => y _ /eqP<- xEy. by have /norP[_ /negPn] := tree_x y xEy; apply: connect_trans. pose fxq1 := [pred y in fx :: q1]; pose y := fx. have{tree_x xEnfx} nfx'y: y != nfx. by apply: contraNneq (tree_x _ xEnfx) => Dy; rewrite !inE -{2}Dy clinkN. suffices{nfx'y} [q2 [_ Lq2 /(conj nfx'y)/norP]]: exists q2, [/\ path clink nfx q2, last nfx q2 = y & ~~ has fxq1 q2]. - by rewrite has_sym /= -/y -Lq2 orbA -in_cons mem_last. have [p2 []]: exists p2, [/\ fpath edge y p2, last y p2 = nfx & z1 \notin p2]. have /connectP[_ /shortenP[p z1Ep /andP[p'z1 _] _] Lp]: cedge z1 nfx. by rewrite cedgeC cedge1 faceK; apply/connectP; exists p1. have p1p_fx: fx \in (x :: p1) ++ p. apply: etrans xEfx; apply/esym/fconnect_cycle; last exact: mem_head. by rewrite /= rcons_path cat_path xEp1 z1Ep last_cat -Lp /= faceK. move: p1p_fx z1Ep p'z1 Lp; rewrite mem_cat (negPf p1'fx). case/splitPr: p / => p p2; rewrite cat_path /= => /and3P[_ _ fxEp2]. by rewrite mem_cat last_cat => /norP[_ /norP[_]]; exists p2. elim: p2 y => [|_ p IHp y /andP[/eqP<- /IHp{}IHp Lp]]; first by exists nil. rewrite inE => /norP[ey'z1 /(IHp Lp){p Lp}IHp]. apply: (@proj2 (y != nfx)); pose fey := face (edge y). have /connectP[q]: fconnect node y fey by rewrite cnode1r edgeK. elim: q (y) => /= [_ _ <- | _ q IHq z /andP[/eqP<- /IHq-IHz] /IHz{IHq IHz IHp}]. have [q2 [nfxCq2 Lq2 q1'q2]] := IHp; suffices fxq1'fey: ~~ fxq1 fey. split; first by rewrite -Lq1 (memPnC fxq1'fey) ?mem_last. exists (rcons q2 fey); rewrite last_rcons rcons_path nfxCq2 Lq2 clinkF. by rewrite has_rcons negb_or fxq1'fey. apply: contra q1'q2 => /z1Fq1/=; rewrite inE eq_sym (negPf ey'z1) /= => q1ey. apply/hasP; exists (edge y); rewrite /= ?mem_belast //. have /predU1P[Dey | //]: edge y \in nfx :: q2 by rewrite -Lq2 mem_last. by rewrite lastI Lq1 -Dey rcons_uniq q1ey in Uq1. case=> nfx'nz [q3 [/shortenP[q2 nfxCq2 /=/andP[q2'nxf Uq2] sq23] Lq2 q1'q3]]. have{q q3 q1'q3 sq23} q1'q2: ~~ has fxq1 q2. by apply: contra q1'q3; rewrite ![has fxq1 _]has_sym; apply: sub_has. suffices fxq1'z: ~~ fxq1 z. split; first by rewrite -Lq1 (memPnC fxq1'z) ?mem_last. exists (rcons q2 z); rewrite last_rcons rcons_path Lq2 clinkN. by rewrite nfxCq2 has_rcons negb_or fxq1'z. rewrite /= inE -(inj_eq nodeI) (negPf nfx'nz) /=. apply: contra (JordanG (fx :: q1 ++ q2)) => q1z; apply/and3P. rewrite cat_path last_cat fxCq1 Lq1 nfxCq2 -/nfx -cat_cons cat_uniq Uq1 q1'q2. by rewrite Lq2 (finv_f nodeI) mem2r_cat // -Lq1 mem2_last. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup)