proposition: Lemma emb_roots_inj : {in froots node &, injective f}.
proof: Proof. move => x y root_x root_y /eqP. rewrite -emb_vertex //. move => /rootP - /(_ cnodeC). by rewrite (eqP root_x) (eqP root_y). 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)