proposition: Lemma n_compEord_seq e (s : seq 'I_n) (a : {pred 'I_n}) : connect_sym e -> closed e a -> s =i a -> n_comp e a = n_comp_ord e s.
proof: Proof. move=> sym_e cl_a eq_a_s; rewrite -(eq_n_comp_r eq_a_s). rewrite (eq_n_comp (eq_connect (eq_sseq e))). apply: n_comp_dfsP; rewrite ?card_ord //. exact: eq_connect_sym sym_e. by rewrite -(eq_closed (eq_sseq e)) (eq_closed_r eq_a_s). Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)