proposition: Lemma connected_arc (G : sgraph) (s : seq G) x1 x2 : ucycle (--) s -> x1 \in s -> x2 \in s -> x1 != x2 -> sgraph.connected [set z in arc s x1 x2].
proof: Proof. by move=> *; exact/connected_path0/arc_path. Qed.
imports: HB(structures) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(sgraph connectivity minor excluded) fourcolor(hypermap geometry walkup color coloring combinatorial4ct) GraphTheory(set_tac) GraphTheory(hmap_ops smerge embedding arc K4plane)