proposition: Lemma chordless_spoke_ring : chordless r.
proof: Proof. apply/subsetP=> y1 ry1; apply: contraLR isT => /exists_inP[y2] /= /adjP[z y1Fz]. rewrite /rlink => ezFy2 /and3P[ry1'y2 r'y1'y2 /= ry2]. pose q := [:: node y2; edge z; edge (node y1)]. have scycRq: scycle rlink q. rewrite srcycleI //= !ee cface1 nodeK cfaceC ezFy2 /= andbC. rewrite cface1r nodeK cfaceC y1Fz /= cfaceC; rewrite !Er in ry1 ry2. by rewrite -!(same_cface ry2) !(same_cface ry1) connect0 bridgeless_cface. rewrite -(Birkhoff _ scycRq) //; apply/(nontrivial0P _); split. pose t := node (edge (node y1)); exists t; rewrite !inE. have Dt: t = prev r y1. have [_ Ur] := andP scycRr; rewrite /t -{1}[y1](next_prev (simple_uniq Ur)). by rewrite next_spoke_ring ?mem_prev // faceK edgeK. rewrite Er in ry2; rewrite unfold_in /= cfaceC -(same_cface ry2). have xFnt: cface x (node t) by rewrite -Er Dt mem_prev. rewrite (same_cface xFnt) -{2}[t]nodeK -cface1r bridgeless_cface //= orbF. rewrite cfaceC (same_cface ezFy2) cfaceC /= orbC. rewrite -[edge _]nodeK -cface1r bridgeless_cface //=. rewrite -(fclosed1 (diskN_node q)) diskN_E inE /= !inE eqxx !orbT andbT. apply: contra r'y1'y2 => tFy2; rewrite -Dt eq_sym. by apply/eqP/(scycle_cface scycRr); rewrite ?Er. exists (node (node y1)); rewrite !inE andbC -(fclosed1 (diskN_node q)). rewrite -{1}[node y1]ee (diskN_edge_ring geoG) ?inE ?eqxx ?orbT ?unfold_in //=. rewrite !Er in ry1 ry2; rewrite cfaceC -(same_cface ry2) (same_cface ry1). rewrite -{1}[node _]nodeK -cface1 cfaceC bridgeless_cface //= orbF orbC. rewrite (canRL nodeK (nnn _)) -cface1 cfaceC cface1 nodeK bridgeless_cface //=. rewrite cface1 cfaceC (same_cface ezFy2) -next_spoke_ring; last by rewrite Er. by apply: contra ry1'y2 => /(scycle_cface scycRr)->; rewrite ?mem_next ?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)