proposition: Lemma emb_n_comp : n_comp glink D = n_comp (--) G.
proof: Proof. symmetry; have eq_D : D =1 [preim f of G] by []. rewrite (eq_n_comp_r eq_D). apply: adjunction_n_comp => //;[exact: sconnect_sym|exact: glinkC|]. split => [x _|x' y' _]; last exact: emb_gcomp. by exists (emb_inv x); rewrite f_iinv connect0. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)