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