proposition: Lemma two_connected_avoid (G : hypermap) (plainG : plain G) : kconnected_map 2 G -> avoid_one G.
proof: Proof. case => _ tcG z x y Hx Hy. have:= tcG (pred1 z) _; rewrite card1 => /(_ isT) {tcG} tcG. have Nz : cnode z =i fclosure node (pred1 z) by apply/closure1/cnodeC. have PNz : [predC cnode z] =i [predC fclosure node (pred1 z)]. { by move => u; rewrite inE /= Nz. } rewrite in_clink_glink //; last exact/predC_closed/connect_closed/cnodeC. apply: connect_restrict_mono (tcG x y _ _); rewrite -?PNz //. apply/subsetP => u. by rewrite -PNz. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)