proposition: Lemma diskN_chord_ring : diskN cr1 =i [predD diskN r & diskN cr2].
proof: Proof. move=> y; suffices: (y \in diskN cr1) + (y \in diskN cr2) = (y \in diskN r). by rewrite inE /= /in_mem /=; do 3?case: (diskN _ y). have{y} [p xCp ->] := connected_clink x y ccG. have r1'x: x \notin r1 by case/andP: dEx; rewrite /= Dr12 => /norP[]. have r2'ex: edge x \notin r2 by case/andP: dEex; rewrite /= Dr12 => /norP[]. elim/last_ind: p xCp => [_ | p y IHp] /=. rewrite !{1}diskN_E dEx orbT addnC -{1}d2Ee Dcr2 inE /= eq_sym e'id. by rewrite (negPf r1'x) inE /= !mem_head. rewrite last_rcons rcons_path !{1}(fclosed1 (diskN_node _) y) => /andP[xCp pCy]. have:= IHp xCp; have{pCy} [<- //| /(canRL faceK)->] := clinkP pCy. move/node: y => y; rewrite [diskN r in RHS]lock !{1}diskN_E -lock. rewrite {1}d1Ee d2Ee Dcr1 Dcr2 !in_cons (can_eq ee) (canF_eq ee) -Dcr1 -Dcr2. have [-> _ | _] := altP (y =P edge x). by rewrite e'id /= dEex orbT d1Ee inE /= mem_head (negPf r2'ex). have [-> _ | _] /= := altP (y =P x). by rewrite dEx orbT -d2Ee Dcr2 inE /= mem_head (negPf r1'x). have [r_y|] := boolP (y \in r); last rewrite Dr12 => /norP[/=/negPf-> /negPf->]. move/eqP; rewrite (diskN_edge_ring r_y) addn_eq0 !eqb0 !negb_or -andbA. case/and4P=> /= _ /negPf-> _ /negPf->; rewrite !orbF. move: Ur r_y; rewrite -(rot_uniq ix) Dr12 Dr cat_uniq inE orbC /=. by case/and3P=> _ /hasPn/(_ y)/implyP; case: (y \in r2) => /= [/negPf| _ _]->. rewrite -(dEe y) diskN_E ![_ \in diskE r]inE /= !Dr12. rewrite [in RHS]inE !negb_or /=; case r1ey: (edge y \in r1) => /=. rewrite orbC; case: (y \in diskE cr1) => //= _. by rewrite -d2Ee Dcr2 !inE r1ey orbT. case r2ey: (edge y \in r2) => //= [] [<-]. by rewrite -d1Ee {1}inE /= Dcr1 mem_behead. 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)