proposition: Lemma ucycle_embr_ring : ufcycle node embr_ring.
proof: Proof. have [[cycEbGd /simple_uniq UbGd] Iembr] := (andP scycle_embd_ring, embr_inj). have UbGm: uniq (map embdd embd_ring) by rewrite (map_inj_uniq embdd_inj). have UbGr: uniq embr_ring. by rewrite -(map_inj_uniq Iembr) map_embr_ring rev_uniq. rewrite /ucycle UbGr andbT; apply: cycle_from_next => //= w. rewrite -(inj_eq Iembr) -next_map // -(mem_map Iembr) map_embr_ring mem_rev. rewrite next_rev /embr //= /embr_node => /mapP[u bGd_u ->]. rewrite (prev_map embdd_inj) // eq_sym. have [_ /andP[_ /eqP/embdd_inj <-] | /(_ u)/andP[]//] := pickP. by rewrite (inj_eq embdd_inj) -(canF_eq edgeK) [_ == _](prev_cycle cycEbGd). 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)