proposition: Lemma eq_ord_enum : ord_enum_eq = ord_enum n.
proof: Proof. apply:eq_in_pmap => k _. exact: insub_eqE. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)