proposition: Lemma diskF_chord_ring : diskF cr1 =i [predD diskF r & diskF cr2].
proof: Proof. move=> y; rewrite [diskF cr1]lock [cr2]lock !inE -fband_chord_ring !inE -!lock. case: (y \in fband cr2) / (altP hasP) => [[z cr2z yFz] | _]; last first. by rewrite inE /= {1}diskN_chord_ring inE /= orbF andbCA. rewrite orbT andbF (closed_connect (diskF_face _) yFz) inE /= diskN_chord_ring. by rewrite inE /= diskN_E cr2z andbF. 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)