proposition: Lemma emb_ncard : fcard node D = #|G|.
proof: Proof. rewrite /n_comp_mem /predI (eq_card (predIT _)) //=. apply/eqP; rewrite eqn_leq -{1}(card_in_imset emb_roots_inj) max_card /=. pose g := froot node \o (emb_inv). have inj_g : injective g. { apply: (@can_inj _ _ _ f) => x. rewrite /g/=. rewrite -{2}[x]emb_invK. apply/emb_vertexP. by rewrite cnodeC connect_root. } rewrite -(card_imset _ inj_g) subset_leq_card //. apply/subsetP => ? /imsetP [x _ ->]. rewrite /g/=. apply/eqP. apply: root_root. exact: cnodeC. 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)