proposition: Lemma embddE : {in [predC embd_ring], {morph embdd: u / edge u}}.
proof: Proof. move=> u; rewrite inE /= -(mem_map embd_inj) map_embd_ring -embedE. by rewrite -{1}[embd u]e2c (mem_map edgeI) /embdd /= /embd_edge inE /= => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)