proposition: Lemma exists_has_ord (p : {pred 'I_n}) : [exists x : 'I_n, p x] = has p ord_enum_eq.
proof: Proof. by rewrite exists_has ; apply/eq_has_r => x; rewrite mem_enum ord_enum_eqT. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)