proposition: Lemma ucycle_snipr_ring : ufcycle node snipr_ring.
proof: Proof. have Ubr: uniq snipr_ring. by rewrite (@map_uniq _ _ snipr) // map_snipr_ring rev_uniq. rewrite /ucycle Ubr andbT; apply: (cycle_from_next Ubr) => u b_u /=. rewrite -val_eqE /= /snipr_node -/(snipr u) -mem_rev -(next_rev Ur). by rewrite -map_snipr_ring map_f // (next_map inj_snipr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)