proposition: Lemma dfs_start x : x \in dfs g #|T| [::] x.
proof: Proof. by apply/dfsP; exists [::]. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)