proposition: Lemma scycle_chord_ring x : x \in fband r -> edge x \in fband r -> scycle rlink (chord_ring x).
proof: Proof. rewrite /chord_ring; case/fprojP; set y1 := fproj r x => r_y1 xFy1. case/fprojP; set y2 := fproj r _ => r_y2 exFy2. have neq_y21: y2 != y1. apply: contraNneq bridge'G => eq_y21; apply/existsP; exists x. by rewrite (same_cface xFy1) cfaceC -eq_y21. case/andP: scycRr; have [i p1 p2 <- _ Dr] := rot_to_arc Ur r_y2 r_y1 neq_y21. rewrite -(rot_cycle i) -(simple_rot i) Dr /= rcons_cat cat_path /=. rewrite {2}/rlink -(same_connect_r cfaceC xFy1) => /and3P[y2Rp1 p1Rx _]. rewrite -cat_cons -cat_rcons simple_cat -rot1_cons simple_rot => /andP[sFxp1 _]. rewrite /scycle (cycle_path x) /= [rlink _ _]p1Rx y2Rp1 [rlink _ _]exFy2. by rewrite /simple /= (rootP cfaceC xFy1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)