proposition: Lemma connected_path0 (G : sgraph) (p : seq G) : path0 (--) p -> sgraph.connected [set z in p].
proof: Proof. case: p => [|x p] => [_|/= pth_p]; first exact: connected0. have -> : x::p = nodes (Path_of_path pth_p) by rewrite nodesE. exact: connected_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)