proposition: Lemma Jordan_WalkupE : Jordan G -> Jordan G'.
proof: Proof. pose t := finv node z; have GnK := finv_f (@nodeI G). have [nt_z zCt]: node t = z /\ clink z t by rewrite -(f_finv nodeI z) clinkN. pose clink1 x y := (x == node y) || (skip1 face x == y). pose clink2 x y := (x == skip1 node y) || (skip1 face x == y). have cpath1I x p: path clink2 x p -> t \notin p -> path clink1 x p. move=> xCp p't; apply/(pathP z)=> i ltip; rewrite /clink1 orbC. have:= pathP z xCp i ltip; rewrite /clink2 orbC; case: (_ == _) => //=. by rewrite (canF_eq GnK) ifN // (memPn p't) ?mem_nth. have cpathI x p: path clink1 x p -> fz \notin p -> path clink x p. move=> xCp p'fz; apply/(pathP z)=> i ltip; apply/clinkP/pred2P. have:= pathP z xCp i ltip; rewrite /clink1 /=; case: (_ == node _) => //=. by case: ifP => // _ /idPn[]; rewrite (memPnC p'fz) ?mem_nth. have cpath1P x p: path clink1 x p -> ~~ path clink x p -> uniq p -> exists p1, exists p2, [/\ fz \in p, p = p1 ++ p2, last z p2 = last x p, path clink x (rcons p1 z) & path clink z p2]. - move=> xCp not_xCp Up; have p_fz: fz \in p by apply: contraR (cpathI x p _) _. rewrite p_fz; case/splitPr: p_fz Up xCp not_xCp => p1 p2; rewrite !cat_path. rewrite /= cat_uniq => /and4P[_ /norP[p1'fz _] p2'fz _] /and3P[p1P p1Cfz p2P]. have [xCp1 fzCp2]: path clink x p1 /\ path clink fz p2 by rewrite !cpathI. rewrite xCp1 fzCp2 andbT /= => /clinkP/pred2P-not_p1Cfz. exists p1, (fz :: p2); rewrite last_cat /= clinkF rcons_path xCp1; split=> //. by apply: contraLR p1Cfz => /norP[_ /= z'fp1]; rewrite /clink1 /= ifN. move=> JordanG [|u q] //; apply/and3P=> -[Uq uCq qvnu]. pose x := val u; pose y := val (finv node (last u q)); pose p := map val q. have Lp: last x p = skip1 node y by rewrite last_map -(f_finv nodeI (last u q)). have{qvnu} pynx: mem2 p y (skip1 node x) by rewrite -(mem2_map val_inj) in qvnu. rewrite /= !(canF_eq GnK) -/t in Lp pynx. have{Uq} Uzp: uniq ([:: z] ++ x :: p). rewrite -map_cons cons_uniq (map_inj_uniq val_inj). by rewrite -has_pred1 has_map (eq_has z'G') has_pred0. have{uCq} xCp: path clink2 x p; last move {u q} in (p) (x) (y) Uzp xCp pynx Lp. apply: etrans uCq; apply: map_path pred0 _ _ _ _; last by rewrite has_pred0. by move=> v w; rewrite (sameP clinkP pred2P). have [p'x Up]: x \notin p /\ uniq p by case/and3P: Uzp. have y'x: x != y by rewrite (memPnC p'x) // (mem2l pynx). have not_xCp: ~~ path clink x p. apply: contra (JordanG (x :: p)) => {} xCp; rewrite /= p'x Up xCp /=. case: eqP => [y_t | _] in Lp; rewrite Lp GnK; last first. case: eqP => // x_t in pynx; have/and3P[] := JordanG [:: z, x & p]. by rewrite Uzp /= Lp GnK -cat1s mem2_cat pynx orbT xCp x_t zCt. have/and3P[] := JordanG (x :: rcons p z); rewrite last_rcons -/t -y_t. rewrite rcons_path xCp Lp clinkN -cats1 -cat_cons uniq_catC Uzp. by rewrite -y_t ifN // in pynx; rewrite mem2_cat pynx. have{y'x} {}not_xCp: ~~ path clink1 x p. apply/negP=> /cpath1P[] {not_xCp}// p1 [p2 [_ Dp Lp2 xCp1 zCp2]]. rewrite Dp -cat_cons uniq_catCA in Uzp. have /and3P[] := JordanG (x :: p1 ++ z :: p2); rewrite Uzp last_cat /= Lp2. split=> //; first by rewrite -cat_rcons cat_path xCp1 last_rcons. case: eqP => [y_t | _] in Lp; rewrite Lp GnK; last first. do [rewrite Dp; case: eqP => [x_t|_]] in pynx; last by rewrite mem2_splice1. rewrite mem2_cat x_t nt_z mem_head andbT; apply/orP; right. apply: contraR (JordanG (z :: p2)) => p1'y; rewrite mem2l_cat // in pynx. by apply/and3P; rewrite (subseq_uniq _ Uzp) ?suffix_subseq // Lp2 Lp GnK. rewrite mem2_cat mem2_cons eqxx /= mem_behead ?orbT //=. apply: contraR (JordanG (x :: rcons p1 z)) => p2'nx; apply/and3P. rewrite xCp1 last_rcons -cats1 (subseq_uniq _ Uzp) ?catA ?prefix_subseq //. by rewrite -y_t ifN // Dp mem2r_cat // y_t in pynx; rewrite mem2_cat pynx. have p_t: t \in p by apply: contraR (cpath1I x p _) _. have{p'x} {}pynx: mem2 p y (node x) by rewrite ifN ?(memPnC p'x) in pynx. do [have{p p_t} [p1 p2] := splitPr p_t] in Uzp Up Lp xCp not_xCp pynx. rewrite !cat_path cat_uniq /= has_sym -cons_uniq in Up xCp not_xCp. have [[xCp1 p1Ct tCp2] [Up1 /norP[p1't Up21] Utp2]] := (and3P xCp, and3P Up). have{xCp Up} [p2't Up2]: t \notin p2 /\ uniq p2 by case/andP: Utp2. have{p1't} {}xCp1: path clink1 x p1 by rewrite cpath1I. have{p2't cpath1I} {}tCp2: path clink1 t p2 by rewrite cpath1I. have{not_xCp p1Ct} Lp1: last x p1 = node z. case/predU1P: p1Ct => [-> /= | p1Ft]; first by rewrite nt_z eqxx. by rewrite xCp1 tCp2 /clink1 p1Ft orbT in not_xCp. have{Lp} [Lp2 t'y]: last t p2 = node y /\ y != t. case: ifPn Lp Uzp; rewrite (lastI x) last_cat => //= _ -> /nandP[]; right. by rewrite belast_cat Lp1 rcons_uniq mem_cat mem_head orbT. have{Up21} {}xCp1: path clink x p1. apply/idPn=> /cpath1P[] {xCp1}// q1 [q2 [p1fz Dp1 Lq2 xCq1 zCq2]]. rewrite {}Dp1 cat_uniq -catA -cat_cons uniq_catCA catA cats1 in Up1 Uzp pynx. have{p1fz} {}tCp2: path clink t p2 by rewrite cpathI ?(hasPn Up21). have q2'nx: node x \notin q2. apply: contra (JordanG (x :: rcons q1 z ++ q2)) => q2nx; apply/and3P. rewrite (subseq_uniq _ Uzp) ?catA ?prefix_subseq // last_cat cat_path xCq1. by rewrite last_rcons Lq2 Lp1 GnK mem2_cat mem_rcons mem_head q2nx orbT. have q2y: y \in q2. apply: contraR (JordanG ((x :: rcons q1 z) ++ t :: p2)) => q2'y. apply/and3P; rewrite (subseq_uniq _ Uzp) ?cat_subseq ?suffix_subseq //. rewrite -/cat last_cat cat_path xCq1 last_rcons /= zCt Lp2 GnK. by rewrite cat_rcons mem2_splice1 //; rewrite mem2lr_splice in pynx. have{q2'nx pynx Up1} p2nx: node x \in t :: p2. rewrite mem2l_cat in pynx; last by case/and3P: Up1 => _ /hasPn->. by apply/implyP: q2'nx; rewrite implyNb -mem_cat (mem2r pynx). case/splitPr: q2 / q2y Uzp Lq2 zCq2 => q21 q22 Uzp. rewrite last_cat cat_path Lp1 /= => Lq22 /and3P[_ _ yCq22]. have/and3P[] := JordanG (x :: rcons q1 z ++ (t :: p2) ++ y :: q22). rewrite -cat_cons uniq_catCA uniq_catC -catA !cat_path !last_cat last_rcons. rewrite (subseq_uniq _ Uzp) ?cat_subseq ?suffix_subseq // mem2_cat mem_cat /=. by rewrite Lp2 Lq22 GnK mem_rcons mem_head p2nx orbT clinkN xCq1 zCt tCp2. have /cpath1P[]: ~~ path clink t p2 => {Up2 tCp2}// [|q1 [q2 [_ Dp2]]]. apply: contra (JordanG (x :: p1 ++ [:: z] ++ t :: p2)) => tCp2. apply/and3P; rewrite -cat_cons uniq_catCA Uzp last_cat cat_path /= Lp1 Lp2. by rewrite xCp1 clinkN zCt GnK mem2_splice1. rewrite {}Lp2 {p2}Dp2 -!cat_cons cat_uniq in Utp2 Uzp pynx * => Lq2 tCq1 zCq2. have{Utp2} Uq21: ~~ has (mem q2) (t :: q1) by rewrite has_sym; case/and3P: Utp2. rewrite [_ ++ _ ++ q2]catA uniq_catCA -catA in Uzp. have q1'y: y \notin t :: q1. apply: contra (JordanG (t :: rcons q1 z ++ q2)) => q1y; apply/and3P. rewrite cat_path tCq1 last_cat last_rcons cat_rcons Lq2 GnK nt_z. rewrite (subseq_uniq _ Uzp) ?suffix_subseq //. by have:= q1y; rewrite mem2_cat mem_head orbC inE (negPf t'y) => /= ->. have q1nx: node x \in t :: q1. apply: contraR (JordanG (x :: p1 ++ z :: q2)) => q1'nx; apply/and3P. rewrite mem2lr_splice // in pynx. rewrite -cat_cons (subseq_uniq _ Uzp) ?cat_subseq ?suffix_subseq //. by rewrite cat_path last_cat /= Lp1 Lq2 GnK xCp1 clinkN mem2_splice1. have{q1'y pynx Uq21} p1y: y \in p1. rewrite catA mem2r_cat ?(hasPn Uq21) // in pynx. by apply/implyP: q1'y; rewrite implyNb orbC -mem_cat (mem2l pynx). case/splitPl: q1 / q1nx => q11 q12 Lq11 in tCq1 Uzp. have/and3P[] := JordanG (t :: q11 ++ (x :: p1) ++ z :: q2). rewrite -cat_cons uniq_catCA (subseq_uniq _ Uzp) ?cat_subseq ?prefix_subseq //. rewrite !cat_path Lq11 catA last_cat /= Lq2 GnK nt_z Lp1 !clinkN xCp1. have ->: path clink t q11 by move: tCq1; rewrite rcons_cat cat_path => /andP[]. by rewrite mem2_cat mem_head mem_cat inE p1y !orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)