proposition: Lemma ring_disk_closed : cubic G -> Kempe_closed (ring_trace bGd).
proof: Proof. move=> cubicG et; move/rev_ring_cotrace=> tr_et. have geoGrr: (ucycle_planar_plain_quasicubic (rotr 1 bGrr)). split; last exact: (planar_snipr planarG scycRrr). split; last by rewrite /ucycle rot_cycle rotr_uniq; case: ppGr. split; first by have:= plainG; rewrite (plain_patch ppGr) => /andP[]. have:= cubicG; rewrite (cubic_patch ppGr) => /andP[_]; apply: etrans. by apply: eq_subset => x; rewrite !inE mem_rotr. have{tr_et} [tr_et [w etMw rUw]] := Kempe_map geoGrr tr_et. split=> [g | {tr_et}]; first exact/rev_ring_cotrace. by exists w => {et etMw}// et /rUw/rev_ring_cotrace. 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)