proposition: Lemma diskN_rev_ring : diskN (rev_ring r) =i [predC diskN r].
proof: Proof. case: pick_in_ring => [y r_y] x; move: r_y; rewrite inE /= -(ee y). have{y} [p xCp ->] := connected_clink x (edge y) ccG. elim: p x xCp => [|y p IHp] x /= => [_ r'ex | /andP[xCy yCP] Lp]. by rewrite diskN_E inE /= mem_rev_ring r'ex /= -(ee x) diskN_edge_ring. have [-> | fxy] := clinkP xCy. by rewrite -!(fclosed1 (diskN_node _) y) //; apply: IHp. rewrite diskN_E mem_rev_ring. case r_ex: (edge x \in r); first by rewrite -[x]ee diskN_edge_ring. rewrite (fclosed1 (diskE_edge geoG scycRrr)) diskN_E inE /= mem_rev_ring ee. rewrite negb_or; apply: andb_id2l => r'x. rewrite (fclosed1 (diskE_edge geoG scycRr)) inE /= r_ex /=. by rewrite (canRL edgeK (ee x)) fxy -!(fclosed1 (diskN_node _)); apply: IHp. 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)