proposition: Lemma fband_spoke_ring y : (y \in fband r) = adj x y.
proof: Proof. apply/hasP/adjP => [[z rz zFy] | [z xFz zRy]]. by exists (node z); [rewrite -Er | rewrite /rlink cface1 nodeK cfaceC]. by exists (face (edge z)); [rewrite Er edgeK | rewrite -cface1r cfaceC]. 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)