proposition: Lemma ucycle_snipd_ring : ufcycle edge snipd_ring.
proof: Proof. have UbGd: uniq snipd_ring. by rewrite -(map_inj_uniq inj_snipd) map_snipd_ring Ur. rewrite /ucycle UbGd andbT; apply: (cycle_from_next UbGd) => u b_u. apply/eqP/inj_snipd; rewrite /= /snipd_edge -/(snipd u) -map_snipd_ring. by rewrite (mem_map inj_snipd) b_u (next_map inj_snipd UbGd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)