proposition: Lemma two_connected_avoid_one : 2.-connected G -> avoid_one D.
proof: Proof. case => cardG sepG z x y cNzx cNzy. have sepN : ~ vseparator [set f z] by move/sepG; rewrite cards1. gen have N1,_ : x cNzx / f x \notin [set f z]. by rewrite inE -emb_vertex // cnodeC. have [p Ip av_p] := avoid_nonseperator sepN (N1 _ cNzx) (N1 _ cNzy). rewrite disjoint_sym disjoints1 in av_p. suff : connect (restrict [set v | f v \in p] clink) x y. { apply/connect_restrict_mono/subsetP => v; rewrite !inE. by apply: contraTN; rewrite (emb_vertex emb_f) => /eqP <-. } have [q [Q1 Q2 Q3]] := emb_path_f p. apply/connectP; exists q; last by rewrite Q2. apply: path_rpath => //; first by rewrite inE. move => z' /Q3; by rewrite inE. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)