proposition: Theorem planar_Jordan G : planar G -> Jordan G.
proof: Proof. move: {-1}_.+1 (ltnSn #|G|) => m; elim: m G => // m IHm G leGm planarG [//|]. have{leGm} ltG'm (z : G) : #|WalkupE z| < m by rewrite -card_S_Walkup. have IHe z := IHm (WalkupE z) (ltG'm z) (planar_WalkupE z planarG). have IHn z := IHm (WalkupN z) (ltG'm z) (planar_WalkupN z planarG). have{m IHm ltG'm} IHf z := IHm (WalkupF z) (ltG'm z) (planar_WalkupF z planarG). have injG z : injective (val : WalkupE z -> G) := val_inj. pose ofG (z x : G) : x != z -> WalkupE z := sub x. have uniqG z := map_inj_uniq (injG z); have mem2G z := mem2_map (injG z). have clink_eq := sameP clinkP pred2P. pose map_cpath f x p := {q | (f q.1, map f q.2) = (x : G, p) & cpath q.1 q.2}. pose lift_cpath z H f x p := z \notin x :: p -> cpath x p -> map_cpath H f x p. have liftE z x p: lift_cpath z (WalkupE z) val x p. rewrite /lift_cpath -has_pred1 /= => /norP[z'x]; pose u := ofG z x z'x. elim: p => [|y p IHp] /= in x z'x u *; first by exists (u, nil). case/norP=> z'y _ /andP[xCy /IHp[]// [v q] /= [Dv Dq] vCq]. exists (u, v :: q); rewrite /= ?clink_eq -?val_eqE /= Dv ?Dq //. by have [<- | ->] := clinkP xCy; rewrite (negPf z'x, negPf z'y) eqxx ?orbT. have liftN z x p: face z \notin p -> lift_cpath z (WalkupN z) val x p. rewrite /lift_cpath -!has_pred1 /= => fz'p /norP[z'x]; pose u := ofG z x z'x. move: fz'p; elim: p => [|y p IHp] /= in x z'x u *; first by exists (u, nil). case/norP=> fz'y _ /norP[z'y _] /andP[xCy /IHp[]// [v q] /= [Dv Dq] vCq]. exists (u, v :: q); rewrite /= ?clink_eq -?val_eqE /= Dv ?Dq //. rewrite (canF_eq (canF_sym faceK)) (negPf fz'y). have [<- | ->] := clinkP xCy; last by rewrite orbC ifN ?eqxx. by rewrite (negPf z'x) if_same eqxx. have liftF z x p: face (edge z) \notin p -> lift_cpath z (WalkupF z) val x p. rewrite /lift_cpath -!has_pred1 /= => fez'p /norP[z'x]; pose u := ofG z x z'x. move: fez'p; elim: p => [|y p IHp] /= in x z'x u *; first by exists (u, nil). case/norP=> fez'y _ /norP[z'y _] /andP[xCy /IHp[]// [v q] /= [Dv Dq] vCq]. exists (u, v :: q); rewrite /= ?clink_eq -?val_eqE /= Dv ?Dq //. rewrite !(canF_eq nodeK) ifN_eq //. have [<- | ->] := clinkP xCy; first by rewrite eqxx. by rewrite (negPf fez'y) (negPf z'y) if_same eqxx orbT. move=> x p; have [t Lp]: {t | last x p = node t} := exist _ _ (esym (edgeK _)). apply/and3P; rewrite Lp (finv_f nodeI) => -[/=/andP[p'x Up] xCp ptnx]. have /predT_subset-sGp: G \subset x :: p. apply/subsetPn=> -[z _ p'z]; have /liftE[//| [u q] /= [Du Dq] uCq] := p'z. have z't: t != z by rewrite (memPn p'z) // mem_behead ?(mem2l ptnx). have Lq: last u q = node (ofG z t z't). by apply/injG; rewrite -last_map /= Du Dq /= -Lp ifN ?(memPn p'z) ?mem_last. case/and3P: (IHe z (u :: q)); rewrite Lq (finv_f nodeI) -mem2G -uniqG /= Dq. by rewrite Du p'x ifN // (memPn p'z) // mem_behead ?(mem2r ptnx). have oG: #|G| = (size p).+1 by rewrite -(eq_card sGp) (card_uniqP _) //= p'x. case: p Up xCp => //= y p /andP[p'y Up] /andP[xCy yCp] in ptnx p'x Lp sGp oG *. have x'y: y != x by rewrite (memPn p'x) ?mem_head. have x't: t != x by rewrite (memPn p'x) ?(mem2l ptnx). have x'nt: node t != x by rewrite -Lp (memPn p'x) ?mem_last. case: p => [|z p] /= in ptnx p'x p'y Up yCp Lp sGp oG *. by rewrite mem2_seq1 Lp (inj_eq nodeI) andbC eq_sym (negPf x't) in ptnx. have y'nt: node t != y by rewrite -Lp (memPn p'y) ?mem_last. have{xCy} Dfx: face x = y. case/clinkP: xCy => // Dny; have /liftE[//| [u q] /= [Du Dq] uCq] := p'x. have Lq: finv node (last u q) = ofG x t x't. by apply/(canLR (finv_f nodeI))/injG; rewrite -last_map /= Du Dq /= ifN. case/and3P: (IHe x (u :: q)); rewrite Lq -mem2G -uniqG /= Du Dq -Dny eqxx p'y. by rewrite mem2_cons ifN // -(inj_eq nodeI) -Dny eq_sym in ptnx. have{yCp Up} [[yCz zCp] [p'z Up]] := (andP yCp, andP Up). move: ptnx p'x; rewrite !inE !negb_or mem2_cons => ptnx /and3P[y'x z'x p'x]. have z'y: y != z by rewrite (memPnC p'y) ?mem_head. have{yCz} Dfy: face y = z. case/clinkP: yCz => // Dnz; pose u : WalkupN y := ofG y x y'x. have /liftF[|//| [v q] /= [Dv Dq] vCq] := p'y; first by rewrite Dnz nodeK. have Lq: finv node (last v q) = insubd v t. apply/(canLR (finv_f nodeI))/injG; rewrite -last_map Dq /= val_insubd /= Dv. by rewrite Lp; case: (t =P y) => [-> | _]; rewrite /= -?Dnz ?eqxx ?ifN. case/and3P: (IHf y (u :: v :: q)); rewrite Lq -mem2G -uniqG /= val_insubd Dq. rewrite vCq clink_eq -!val_eqE /= Dv Dnz nodeK !(inj_eq nodeI) -Dnz eqxx. rewrite -Dfx (inj_eq faceI) Dfx (negPf x'y) (negPf z'x) (negPf z'y) !eqxx. move: ptnx; rewrite orbT !negb_or p'x p'z inE Dnz (inj_eq nodeI) (negPf z'x). by rewrite eq_sym; case: ifP; rewrite // mem2_cons eqxx. have Dt: t = y. have /liftE[//| [v q] /= [Dv Dq] vCq] := p'y. apply: contraNeq (IHe y (ofG y x y'x :: v :: q)) => y't; apply/and3P. have ->: finv node (last v q) = ofG y t y't. by apply/(canLR (finv_f nodeI))/injG; rewrite -last_map /= Dv Dq /= ifN. rewrite -mem2G -uniqG /= clink_eq orbC -val_eqE /= Dv Dq Dfx Dfy !eqxx /=. split=> //; first by rewrite negb_or z'x p'x p'z. by rewrite ifN_eqC // in ptnx; rewrite ifN // (memPn p'y) ?(mem2r ptnx). move: ptnx Lp x'nt y'nt; rewrite {t x't}Dt eqxx /= => p_nx Lp x'ny y'ny. have{p_nx} Dnx: node x = y. have /liftN[|//| [v q] /= [Dv Dq] vCq] := p'y; first by rewrite Dfy. apply: contraNeq (IHn y (ofG y x y'x :: v :: q)) => y'nx; apply/and3P. have ->: finv node (last v q) = v. apply/(canLR (finv_f nodeI))/injG; rewrite /= -last_map Dv Dq ifN //. by rewrite Lp -Dfy faceK eqxx. rewrite -mem2G -uniqG /= clink_eq -!val_eqE /= Dv Dq negb_or z'x p'x p'z. rewrite (negPf y'ny) vCq -Dfy faceK Dfy Dfx !eqxx orbT; split=> //. rewrite -(inj_eq faceI) nodeK Dfy !ifN // mem2_cons eqxx /=. by rewrite inE (negPf y'nx) /= in p_nx. rewrite inE negb_or z'y /= in p'y. case: p zCp => /= [_ | t p /andP[zCt tCp]] in p'x p'y p'z Up Lp sGp oG *. case/idPn: planarG; rewrite -lt0n half_gt0 ltn_subRL -addnA /Euler_lhs {}oG. have oG1 f: injective f -> f x = y /\ f y = z -> f z = x /\ fcard f G = 1. move=> injf [Dy Dz]; rewrite -Dy -Dz in sGp; split. by have/predU1P[|/norP[]] := sGp (f z); rewrite ?orbF ?inj_eq ?(eq_sym z). rewrite // -(n_comp_connect (fconnect_sym injf) x). apply/esym/eq_n_comp_r => t; have:= sGp t; rewrite !inE -Dy. by case/or3P=> /eqP->; rewrite -?same_fconnect1_r ?connect0. have [[//|Dfz ->] [//|Dnz ->]]:= (oG1 _ faceI, oG1 _ nodeI). have [|_ ->] := oG1 _ edgeI; first by rewrite -Dnz -{2}Dnx -Dfz -Dfy !faceK. by rewrite !addnS [n_comp _ G](cardD1 (root glink x)) inE (roots_root glinkC). have z'ny: node y != z by rewrite -Lp (memPn p'z) ?mem_last. have{zCt} Dnt: node t = z. case/clinkP: zCt => // Dfz; have /liftE[//| [w q] /= [Dw Dq] wCq] := p'z. have /and3P[] := IHe z [:: ofG z x z'x, ofG z y z'y, w & q]. rewrite mem2_cons -uniqG -(canF_eq (finv_f nodeI)) /= !clink_eq -!val_eqE /=. rewrite -last_map Dw Dq wCq Lp Dfx Dfy Dfz (negPf z'y) !eqxx !orbT. split=> //; first by rewrite negb_or y'x p'x p'y. by rewrite (negPf z'ny) eqxx /= !inE -val_eqE /= Dnx (negPf z'y) eqxx. have /liftF[|//| [w q] /= [Dw Dq] wCq] := p'z. by rewrite -Dnt nodeK; case/andP: Up. have /and3P[] := IHf z [:: ofG z x z'x, ofG z y z'y, w & q]. rewrite mem2_cons -uniqG -(canF_eq (finv_f nodeI)) /= !clink_eq -!val_eqE /=. rewrite (negPf z'ny) -last_map Dw Dq Lp eqxx inE negb_or y'x p'x p'y Up wCq. split=> //; last by rewrite inE -val_eqE /= Dnx (negPf z'y) eqxx. rewrite Dfx (negPf z'ny) -Dfy (inj_eq faceI) Dfy -Dnt !(inj_eq nodeI) nodeK Dnt. by rewrite (eq_sym z) (negPf z'y) !eqxx ifN ?eqxx ?orbT //; case/norP: p'z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup)