proposition: Lemma n_compEord e : connect_sym e -> n_comp e 'I_n = n_comp_ord e (ord_enum_eq).
proof: Proof. move=> sym_s; exact: n_compEord_seq ord_enum_eqT. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)