proposition: Lemma next_spoke_ring (y : G) : y \in r -> next r y = face (spoke y).
proof: Proof. move=> ry; have [cycFp Up] := andP ucycFp. rewrite -{1}[y]nodeK (next_map inj_spoke) ?rev_uniq // (next_rev Up). rewrite -[prev p _]faceK /spoke ee -(canRL nodeK (nnn y)). by rewrite (eqP (prev_cycle cycFp _)) // -Ep -Er. 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)