proposition: Lemma map_embr_ring : map embr embr_ring = rev (map embdd embd_ring).
proof: Proof. apply: map_preim => x; rewrite codom_embr mem_rev => /mapP[u bGd_u ->{x}]. by rewrite inE /= (mem_image embdd_inj) negbK. 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)