proposition: Lemma diskE_edge : fclosed edge diskE.
proof: Proof. apply: (intro_closed cedgeC) => x _ /eqP <- /andP[/= r'x dNx]. suffices[x' dNx' [p [x'Fp <-] /= /norP[r'x' r'p]]]: exists2 x', x' \in diskN & exists2 p, fpath face x' p /\ last x' p = edge x & ~~ has (mem r) (x' :: p). - elim/last_ind: p x'Fp r'p => [|p y IHp] /=; first by rewrite !inE r'x'. rewrite last_rcons rcons_path has_rcons /= => /andP[x'Fp Dy] /norP[r'y r'p]. have{IHp x'Fp r'p} /andP[r'p /hasP[z rz z'Dp]] := IHp x'Fp r'p. rewrite !inE r'y; apply/hasP; exists z => //=; apply: connect_trans z'Dp _. by rewrite connect1 /dlink //= r'p -(eqP Dy) clinkF. pose x' := face (edge x); have: cface x' (edge x) by rewrite cfaceC fconnect1. case/connectP=> _ /shortenP[q x'Fq Uq _] Lq. have [[y qy ry] | r'q] := altP (@hasP _ (mem r) (x' :: q)); last first. by exists x'; [rewrite (fclosed1 diskN_node) edgeK | exists q]. have [i r1 Dr] := rot_to ry. have:= cycRr; rewrite -(rot_cycle i) Dr /= rcons_path => /andP[yRr1]. set z := last y r1; pose z' := face (edge z) => zRy. have rz: z \in r by rewrite -(mem_rot i) Dr mem_last. have yFz': cface y z' by rewrite cfaceC -cface1. have: z' \in x' :: q. suffices Fx': cface x' =i x' :: q. by rewrite -!Fx' [_ \in _]cfaceC (same_cface yFz') -cfaceC in qy *. by apply: fconnect_cycle (mem_head _ _); rewrite /= rcons_path x'Fq -Lq /=. rewrite inE => /predU1P[/faceI/edgeI zx | qz']; first by rewrite -zx rz in r'x. rewrite {}Lq; do [have{q qz'} [q1 q2] := splitPr qz'] in Uq x'Fq qy *. rewrite -cat_cons cat_uniq mem_cat cat_path last_cat in Uq x'Fq qy *. rewrite /= in x'Fq *. have{Uq x'Fq} [[Uq1 Uq12 Uq2] [x'Fq1 /eqP Lq1 zFq2]] := (and3P Uq, and3P x'Fq). have{qy} [q1y | q2y] := orP qy. exists z'; last exists q2 => //. by rewrite (fclosed1 diskN_node) edgeK diskN_E inE /= rz. apply: contra Uq12 => /(@hasP _ _ (z' :: q2))[t q2t rt]. have yFt: cface y t by apply: connect_trans (path_connect zFq2 _). by apply/hasP; exists y => //; rewrite (scycle_cface scycRr ry rt yFt). pose rclink := [fun t => face (if t \in r then edge t else t)]. have [c [z'Cc Uc Lc] [sr1c Uq1c]]: exists2 c, [/\ fpath rclink z' c, uniq (z' :: c) & last z' c = z] & {subset y :: r1 <= z' :: c} /\ ~~ has (mem (x' :: q1)) (z' :: c). have sr1r: {subset r1 <= r}. by move=> t r1t; rewrite -(mem_rot i r) Dr mem_behead. have cFpL (t : G) c : fpath face t c -> {subset t :: c <= cface (last t c)}. move=> tFc u cu; apply: connect_trans (path_connect tFc cu). by rewrite cfaceC; apply/connectP; exists c. have sFCr t c : uniq (t :: c) -> last t c \in r -> fpath face t c -> fpath rclink t c. - rewrite lastI rcons_uniq => /andP[Uc _] Lc tFc. have RFbase: fun_base id rclink face (mem r) by move=> u v /= /negPf->. rewrite -(map_id c) (map_path RFbase) // -(@eq_has _ (mem r)) //. apply/hasPn=> u cu; apply: contra Uc => /= ru. by rewrite (scycle_cface scycRr Lc ru) // [cface _ _]cFpL ?mem_belast. have /=/andP[r1'y Ur1]: uniq (y :: r1) by rewrite -Dr rot_uniq. suffices [c2 [yRc2 Uc2 Lc2] [sr1c2 sFc2r1]]: exists2 c2, [/\ fpath rclink y c2, uniq c2 & last y c2 = z] & {subset r1 <= c2} /\ {subset fband c2 <= fband r1}. - have c2F'y t: t \in c2 -> ~~ cface y t. move=> c2t; apply: contra r1'y => yFt. have /hasP[u r1u tFu]: has (cface t) r1 by apply/sFc2r1/hasP; exists t. by rewrite (scycle_cface scycRr _ _ (connect_trans yFt tFu)) // sr1r. case/splitPl: {q2}q2y zFq2 Uq12 Uq2 => c1 q2' Lc1. rewrite cat_path -cat_cons has_cat cat_uniq => /andP[z'Fc1 _]. move=> /norP[Uq1c1 _] /andP[Uc1 _]. exists (c1 ++ c2). rewrite cat_path last_cat Lc1 -cons_uniq -cat_cons cat_uniq Uc1 Uc2 andbT. rewrite sFCr ?Lc1 //; split=> //; apply/hasP => [[t c2t c1t]]. by case/negP: (c2F'y t c2t); rewrite -Lc1 [cface _ t]cFpL. rewrite -cat_cons has_cat orbA negb_or Uq1c1; split. move=> t /predU1P[-> | r1t]; rewrite mem_cat -?Lc1 ?mem_last //. by rewrite sr1c2 ?orbT. apply/hasP => [[t c2t q1t]]; case/negP: (c2F'y t c2t). by rewrite (same_cface yFz') -Lq1 -cface1 [cface _ _]cFpL. rewrite {i Dr z' zRy rz yFz' Uq12 Uq2 Lq1 zFq2 q2y r1'y}/z. elim: r1 y ry sr1r yRr1 Ur1 => /= [|z r1 IHr] y ry; first by exists nil. move/allP=> /=/andP[rz /allP sr1r] /andP[yRz zRr1] /andP[r1'z Ur1]. have{IHr zRr1 Ur1}[c2 [zRc2 Uc2 Lc2] [sr1c2 sc2r1]] := IHr z rz sr1r zRr1 Ur1. move: yRz; rewrite /rlink cface1 => /connectP[_ /shortenP[c1 yFc1 Uc1 _] Lc1]. have sc1Fz := cFpL _ _ yFc1; rewrite -Lc1 in sc1Fz. exists ((face (edge y) :: c1) ++ c2). split; last by rewrite last_cat /= -Lc1. by rewrite cat_path /= -Lc1 zRc2 andbT {1}/rclink /= ry eqxx sFCr -?Lc1. rewrite cat_uniq Uc1 Uc2 andbT; apply: contra r1'z => /hasP[t c2t c1t]. have /hasP[u r1u tFu]: fband r1 t by apply/sc2r1/hasP; exists t. have zFu: cface z u := connect_trans (sc1Fz t c1t) tFu. by rewrite (scycle_cface scycRr rz _ zFu) ?sr1r. split=> t. rewrite inE mem_cat => /predU1P[-> | r1t]; first by rewrite Lc1 mem_last. by rewrite orbC sr1c2. rewrite [t \in _]has_cat => /orP[/hasP[u c1u tFu] | /sc2r1/hasP[u r1u tFu]]. apply/hasP; exists z; first exact: mem_head. by rewrite (same_cface tFu) cfaceC [cface _ _]sc1Fz. by apply/hasP; exists u; first apply: mem_behead. have [x1 c_nx1 [p [x1Cp Lp] Upc]]: exists2 x1, node x1 \in z' :: c & exists2 p, path clink x1 p /\ last x1 p = x' & ~~ has (mem (z' :: c)) (x1 :: p). - have{dNx} [x0 rx0 /connectP[p x0'Dp Lp]] := hasP dNx. set x0' := finv node x0 in x0'Dp Lp. have cycCc: fcycle rclink (z' :: c) by rewrite /= rcons_path z'Cc /= Lc rz. have{rx0}: has (mem (z' :: c)) (x0' :: p). have cx0: x0 \in z' :: c by rewrite sr1c // -Dr mem_rot. have <-: rclink x0 = x0' by rewrite /= rx0 -[x0](f_finv nodeI) nodeK. by rewrite (eqP (next_cycle cycCc cx0)) /= (mem_next (_ :: _)) cx0. elim: p {x0}x0' x0'Dp Lp => [|x1 p IHp] x0. rewrite /= orbF => _ <-{x0} cx; exists x'; first by rewrite edgeK. exists nil; rewrite //= orbF; apply: contra Uq1c => cx'. by rewrite has_sym /= cx'. rewrite {-1 2 4}[@cons]lock /= -lock orbC => /andP[x0Dx1 x1Dp] Lp. have [cIp _| Ucp {IHp} cx0] := boolP (has _ _); first exact: IHp cIp. have:= cx0; rewrite orFb -mem_next -(eqP (next_cycle cycCc cx0)) /=. case/andP: x0Dx1 => /negPf-> x0Cx1 cfx0. have [x0nx1 | fx0x1] := clinkP x0Cx1; last by rewrite /= -fx0x1 cfx0 in Ucp. exists x1; [by rewrite -x0nx1 | exists (rcons p x')]. split; last by rewrite last_rcons. rewrite rcons_path -Lp /= -{1}[x]edgeK clinkN andbT. by apply: sub_path x1Dp => t u /andP[]. rewrite has_rcons orbCA negb_or Ucp andbT. by apply: contra Uq1c; rewrite has_sym /= => ->. have {}z'Cc: path clink z' c. apply: sub_path z'Cc => t _ /eqP <- /=. by case: ifP => _; [rewrite -{1}[t]edgeK clinkN | rewrite clinkF]. have [c0 [x1Cc0 Lc0] Ucc0]: exists2 c0, path clink x1 c0 /\ clink (last x1 c0) z' & ~~ has (mem (z' :: c)) (x1 :: c0). - exists (p ++ q1). split; last by rewrite last_cat Lp -Lq1 clinkF. by rewrite cat_path x1Cp Lp (sub_path _ x'Fq1) //; apply: subrelUr. rewrite -cat_cons has_cat negb_or Upc. by rewrite has_sym in Uq1c; case/norP: Uq1c. case/shortenP: x1Cc0 Lc0 => [c1 x1Cc1 Uc1 sc01] Lc1. have /and3P[] := planarP G planarG (x1 :: c1 ++ z' :: c); split; first 1 last. - by rewrite cat_path /= x1Cc1 Lc1. - rewrite last_cat /= Lc mem2_cat mem2_cons (finv_eq_can nodeK) -/z'. by rewrite eqxx /= c_nx1 orbT. rewrite -cat_cons cat_uniq Uc1 Uc andbT; apply: contra Ucc0 => /hasP[t ct c1t]. by apply/hasP; exists t; move: c1t; rewrite //= !inE; case: eqP => // _ /sc01. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)