proposition: Lemma scycle_spoke_ring : scycle rlink r.
proof: Proof. have [cycFp Up] := andP ucycFp; apply/andP; split. apply: cycle_from_next; first by rewrite (map_inj_uniq inj_spoke) ?rev_uniq. by move=> y ry; rewrite (next_spoke_ring ry) /rlink -!cface1r. rewrite /simple /r !map_rev rev_uniq -map_comp map_inj_in_uniq // => y z py pz. move/(rootP cfaceC); rewrite -cface1 -cface1r; apply: double_dart. by rewrite -!Ep in py pz; rewrite -(same_cface py). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)