proposition: Lemma mem_spoke_ring y : (y \in spoke_ring) = cface x (node y).
proof: Proof. by rewrite -{1}[y]nodeK (mem_map inj_spoke) mem_rev Ep. 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)