proposition: Lemma emb_roots_bij : {in froots node, bijective f}.
proof: Proof. exists (froot node \o (emb_inv)). - move => x /= /eqP {2}<-; apply/rootP; first exact cnodeC. by rewrite (emb_vertex emb_f) f_iinv. - move => x /= _. rewrite -{2}[x]emb_invK. apply/emb_vertexP. by rewrite cnodeC connect_root. 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)