proposition: Lemma card_emb : #|D| = #|E(G)|.*2.
proof: Proof. by rewrite -emb_ecard -muln2 fcard_order_set //; exact: emb_plain emb_f. 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)