proposition: Lemma connectEdfs x : connect (grel g) x =i connect_dfs x.
proof: Proof. by move=> y;rewrite /connect_dfs kT; apply/connectP/dfsP. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)