proposition: Lemma ord_enum_eqT : ord_enum_eq =i 'I_n.
proof: Proof. by move => i; rewrite eq_ord_enum mem_ord_enum. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)