proposition: Lemma emb_loopless : loopless D.
proof: Proof. apply/existsPn => x. apply: contraNN (negbT (adjn_irrefl x)) => H. apply/exists_inP; exists x => //. exact: connect0. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)