proposition: Lemma two_connected_cyle (G : hypermap) : avoid_one G -> plain G -> loopless G -> planar G -> forall x y : G, x != y -> cface x y -> ~~ cnode x y.
proof: Proof. move => tcG plainG llG planarG x y xDy cf_xy; apply/negP => cn_xy. wlog [p [path_p uniq_p disj_p]] : x xDy cf_xy cn_xy / exists p, [/\ fpath (finv node) y (rcons p x), uniq p & [disjoint p & cface x]]. { move => W. pose o := orbit (finv node) y; pose a := cface x. have [o' def_o] : exists o', o = y :: o' by rewrite /o/orbit -orderSpred /=; eexists. have has_x : has a o'; first (apply/hasP; exists x; last exact: connect0). suff: x \in o by rewrite def_o inE (negPf xDy). by rewrite -fconnect_orbit same_fconnect_finv // cnodeC. case/split_find def_o' : _ _ _ / has_x => [x' p q a_x' hasNp]; subst o'. have: uniq o by apply: orbit_uniq. have: fcycle (finv node) o by apply/cycle_orbit/finv_inj. have cf_x'y: cface x' y by apply: connect_trans cf_xy; rewrite cfaceC. rewrite def_o /= rcons_path cat_path -!andbA => /andP [path_p _]. rewrite cat_uniq rcons_uniq -!andbA mem_cat mem_rcons inE !negb_or -!andbA eq_sym. move => /andP[? /and5P[_ _ _ uniq_p _]]; apply: (W x') => //. - rewrite cnodeC -same_fconnect_finv //; apply/connectP; exists (rcons p x') => //. by rewrite last_rcons. - exists p; split => //; rewrite disjoint_has // (eq_has (_ : cface x' =i cface x)) //. move=> z; rewrite !inE; apply: (same_connect cfaceC). by apply: connect_trans cf_x'y _; rewrite cfaceC. } have := cycle_orbit faceI x; have := orbit_uniq face x. have : y \in orbit face x by rewrite -fconnect_orbit. case def_c : (orbit face x) => [//|x0 c]. move: (def_c). have {def_c} -> : x0 = x by move: def_c; rewrite /orbit -orderSpred; case. move => def_c y_in_c uniq_c cycle_c. rewrite inE eq_sym (negbTE xDy) /= in y_in_c. case/splitP def_c' : {1}c _ _ / y_in_c => [c1 c2]. move: uniq_c. rewrite def_c' /= cat_uniq has_sym has_rcons mem_cat mem_rcons rcons_uniq. rewrite !inE (negbTE xDy) !negb_or /= -disjoint_has -!andbA disjoint_sym. case/and5P => x_c1 x_c2 y_c1 uniq_c1 /and3P [y_c2 dis_c1_c2 uniq_c2]. move: path_p; rewrite rcons_path /= => /andP [path_p /eqP lst_p]. have [u [v] [q] [path_q u_c v_c uniq_q disj_q]]: exists u v q, [/\ path clink u (rcons q v), u \in c2, v \in c1, uniq q & [disjoint q & [predU cface x & p]]]. { have [u [u_c1 Hu]] : exists u, u \in c1 /\ ~~ cnode x u. { destruct c1 as [|a ?]; move: cycle_c cn_xy; rewrite def_c'. - case/andP => /eqP <- _. by rewrite (negbTE (loopless_face _ _ _)). - rewrite rcons_cons /= rcons_path => /and3P [/eqP<- _ _]. exists (face x). by rewrite mem_head loopless_face. } have [v [v_c2 Hv]] : exists v, v \in c2 /\ ~~ cnode x v. { elim/last_ind : c2 def_c' cycle_c cn_xy {x_c2 y_c2 dis_c1_c2 uniq_c2} => [|? a _] /= ->. - rewrite cats0 /= rcons_path last_rcons => /andP [_ /eqP <-]. by rewrite cnodeC (negbTE (loopless_face _ _ _)). - rewrite !(rcons_path,cat_path) /= -!andbA last_cat !last_rcons => /and5P [_ _ _ _ /eqP E ?]. exists (finv face x). by rewrite -E finv_f // mem_rcons mem_head cnodeC loopless_face. } have uDv : v != u. { apply: contraTneq dis_c1_c2 => ?; subst. by apply/pred0Pn; exists u. } have [q [pth_q uniq_q sub_q]] := @connect_inE _ _ _ _ _ uDv (tcG x v u Hv Hu). have [u0 [v0] [q0] [A B C D E]] := disjoint_subpath v_c2 u_c1 pth_q dis_c1_c2. exists u0; exists v0; exists q0; split => //. - apply: subseq_uniq uniq_q. apply: subseq_trans D. exact: subseq_trans (subseq_rcons _ _) (subseq_cons _ _). - move/mem_subseq in D. apply/disjointP => z in_q0; apply/negP; rewrite !inE negb_or fconnect_orbit def_c. have Nz k : cnode y k -> z != k. { move => Nyk. have:= connect_trans cn_xy Nyk. apply contraTneq => <-. by apply/sub_q/D; rewrite !(inE,mem_rcons) in_q0. } rewrite def_c' !(inE,mem_rcons,mem_cat) !negb_or !Nz 1?cnodeC //= -negb_or orbC. move: (disjointFr E in_q0); rewrite inE => -> /=. apply: contraTN (eqxx z) => z_p; apply/Nz. rewrite -same_fconnect_finv //. move/path_connect in path_p. by apply/path_p; rewrite !inE z_p. } case/splitP def_c2 : {1}c2 _ _ / (u_c) => [c21 c22]. pose mp := rcons p x ++ rcons c1 y ++ rcons c21 u ++ q. suff: Moebius_path mp by apply/negP; exact: planarP. move: path_q; rewrite rcons_path => /andP [path_q lst_q]. have/andP [dis_q_f dis_q_p] : [disjoint q & (x::c)] && [disjoint p & q]. { move: disj_q. rewrite disjoint_sym disjointU => /andP [A ->]; rewrite andbT disjoint_sym. by apply: disjointWl A; apply/subsetP => ?; rewrite -def_c -fconnect_orbit. } rewrite /mp headI /Moebius_path -{2}headI /=. apply/and3P; split. - suff: uniq (rcons p x ++ c ++ q). { apply: subseq_uniq. apply: cat_subseq => //. rewrite catA. apply: cat_subseq => //. rewrite def_c' def_c2. apply: cat_subseq => //. exact: prefix_subseq. } rewrite -cats1 -catA [[:: x] ++ _ ++ _]catA cat1s -def_c. rewrite cat_uniq has_cat negb_or -!disjoint_has uniq_p /=. rewrite ![[disjoint _ & p]]disjoint_sym dis_q_p (disjointWr _ disj_p). 2: by apply/subsetP => z; rewrite -fconnect_orbit. rewrite cat_uniq orbit_uniq -disjoint_has disjoint_sym uniq_q /= andbT. by rewrite disjoint_sym def_c. - rewrite !catA cat_path !last_cat last_rcons path_q andbT -catA. rewrite cat_path last_head_behead (_ : path _ _ _) /=. + move/(sub_path sub_face_clink) : cycle_c. by rewrite def_c' def_c2 !rcons_cat catA [in X in X -> _]cat_path => /andP [-> _]. + move/(sub_path sub_node_clink): path_p lst_p. destruct p as [|z p] => //= /andP [A B] <-. by rewrite rcons_path B -{1}[last z p](f_finv nodeI) clinkN. - rewrite 3!last_cat last_rcons. have -> : node (head x p) = y. { move: path_p lst_p. destruct p as [|z p]=> /= [_ <-|/andP[/eqP <- _] _]; exact: f_finv. } suff -> : finv node (last u q) = v. { by rewrite !mem2_cat (_ : mem2 (rcons c1 y) v y) // -cats1 mem2_cat v_c !inE eqxx. } case/clinkP: lst_q => [->|def_v]; first by rewrite ?finv_f. case: notF. have: finv face v \in x::c1. { have : fpath face x c1. { move: cycle_c. rewrite def_c' -cat1s catA /= rcons_cat cat_path rcons_path. by case: (fpath _ _ c1). } case/splitP : v_c => [p1 p2 _]. rewrite cat_path !rcons_path last_rcons -andbA /=. case/and3P => _ /eqP <- _. by rewrite finv_f // -cats1 -catA /= -cat_cons mem_cat mem_last. } rewrite -{}def_v finv_f //. case/last_memE => [|[z Z1]]. + rewrite inE (disjointFr dis_c1_c2) // orbF => E. by rewrite -(eqP E) u_c in x_c2. + rewrite inE; case/predU1P => [?|H]. * subst z. by rewrite (disjointFl dis_q_f) // mem_head in Z1. * by rewrite (disjointFl dis_q_f) // def_c' !(inE,mem_rcons,mem_cat) H in Z1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)