proposition: Lemma diskN_edge_ring x : x \in r -> (edge x \in diskN r) = false.
proof: Proof. move=> r_x; rewrite diskN_E -(fclosed1 (diskE_edge geoG _)) //. rewrite inE /= r_x orbF; apply: contraTF nt_r => r_ex. have Dex: edge x = next r x. by apply: (scycle_cface scycRr) (next_cycle cycRr r_x); rewrite ?mem_next. have Dx: x = next r (edge x). apply: (scycle_cface scycRr); rewrite ?mem_next //. by rewrite -{1}[x]ee; apply: (next_cycle cycRr r_ex). have [i p Dr] := rot_to r_x; rewrite -(proper_ring_rot i) //. move: Dex Dx Ur; rewrite -!(next_rot i Ur) -(rot_uniq i) {i}Dr. case: p => [|y [|z p]] //= ->; rewrite !eqxx ?negbK // !inE eq_sym. by case: ifP => // _ ->; rewrite eqxx. 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)