proposition: Lemma simple_snipd_ring : simple snipd_ring.
proof: Proof. have: uniq snipd_ring by rewrite -(map_inj_uniq inj_snipd) map_snipd_ring. have: all (fun u => snipd u \in r) snipd_ring. by rewrite -all_map map_snipd_ring; apply/allP. rewrite /simple; elim: snipd_ring => //= u p IHp /andP[ru spr] /andP[p'u Up]. rewrite {}IHp {Up}// (contra _ p'u) // => /mapP[v pv uFv]. rewrite (inj_snipd (scycle_cface scycRr ru (allP spr v _) _)) // cface_snipd. exact/(rootP cfaceC). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)