proposition: Lemma fband_chord_ring : [predU fband cr1 & fband cr2] =i fband r.
proof: Proof. move=> y; rewrite Dcr1 Dcr2 !inE !fband_cons orbAC orbA -orbA -fband_cat -Dr. by rewrite fband_rot orb_idl // => /orP[] /(closed_connect (fbandF r))->. 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)