proposition: Lemma adj11_edge y : adj x y -> adj x (edge y) -> (y \in r) || (edge y \in r).
proof: Proof. rewrite -!fband_spoke_ring => /hasP[z rz yFz] /hasP[t rt eyFt]. apply: contraFT (pred0P (subsetP chordless_spoke_ring _ rz) t). case/norP=> r'y r'ey; rewrite !inE -(adjF yFz) -(adjFr eyFt) adjE rt andbT. have [cycRr /simple_uniq Ur] := andP scycRr. rewrite /= andbC eq_sym (canF_eq (next_prev Ur)) !next_spoke_ring //. apply/andP; split; apply/eqP=> Dz. rewrite Dz -!cface1r -[y]ee in yFz. by rewrite (double_dart eyFt) ?rt in r'ey. by rewrite Dz -!cface1r in eyFt; rewrite (double_dart yFz) ?rz in r'y. 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)