proposition: Lemma rev_ring_cotrace et : ring_trace bGd et <-> ring_trace (rotr 1 bGrr) et.
proof: Proof. set pd := snipd_ring planarG scycRr; set pr := rotr 1 bGrr. have eqFpdr: map (froot face) (map snipr pr) = map (froot face) (map snipd pd). rewrite /pd map_snipd_ring // /pr !map_rotr map_snipr_ring map_rev. by rewrite froot_face_rev_ring revK rotK. split=> [[kd [kdE kdF]] | [kr [krE krF]]] ->{et}. pose kr (xr : Grr) := oapp kd Color0 (pick (pfd (snipr xr))). have plainGrr: plain rev_snipr_disk. by move: plainG; rewrite (plain_patch ppGr) => /andP[]. have krF: invariant face kr =1 Grr. move=> xr; apply/eqcP; congr (oapp kd _ _); apply: eq_pick => yd. by apply: same_cface; rewrite -(patch_face_r ppGr) cfaceC fconnect1. have krE xr: snipr xr \notin rev_ring r -> (kr (edge xr) == kr xr) = false. set x := snipr xr => rr'x; rewrite /kr. have{rr'x} /imageP[xd _ Dx]: x \in codom (snipd : Gd -> G). apply/negbNE; rewrite codom_snipd -[_ \notin _]diskN_rev_ring //. by rewrite diskN_E negb_or /= rr'x (valP xr). have [|yd -> xdFyd /=] := @pfdP x xd; first by rewrite Dx. have [|zd -> fexdFzd /=] := @pfdP (edge x) (face (edge xd)). by rewrite Dx -{1}[xd]edgeK cface1 nodeK. rewrite -(fconnect_invariant kdF xdFyd) -(fconnect_invariant kdF fexdFzd). by rewrite (eqcP (kdF _)); apply: kdE. exists kr; [split=> // xr | congr (trace _)]. have [rr_x | /krE//] := boolP (snipr xr \in rev_ring r). rewrite /= eq_sym -{1}[xr]plain_eq //; apply: krE. rewrite !mem_rev_ring in rr_x *. by have:= diskN_edge_ring r_ok rr_x; rewrite ee diskN_E => /norP[]. elim: pd pr eqFpdr => [|xd pd IHpd] [|xr pr] //=. case=> /(rootP cfaceC) xdFxr /IHpd->; congr (_ :: _); rewrite /kr. by have [yd -> xdFyd /=] := pfdP xdFxr; apply: fconnect_invariant xdFyd. pose kd (xd : Gd) := oapp kr Color0 (pick (pfrr (snipd xd))). have kdF: invariant face kd =1 Gd. move=> xd; apply/eqcP; congr (oapp kr _ _); apply: eq_pick => yr. by apply: same_cface; rewrite cface_snipd cfaceC fconnect1. exists kd; [split=> // xd | congr (trace _)]. rewrite /= -(eqcP (kdF (edge xd))) -{2}[xd]edgeK; move: {xd}(face _) => xd. rewrite /kd; set x := snipd xd. have /imageP[nxr _ Dnx]: node x \in codom (snipr : Grr -> G). rewrite codom_snipr // !inE diskN_rev_ring // !inE andbC. by rewrite -(fclosed1 (diskN_node r)) (valP xd). have [|yr -> nxFyr /=] := @pfrrP (node x) nxr; first by rewrite -Dnx. have [|zr -> xFzr /=] := @pfrrP x (edge nxr). by rewrite (canRL nodeK Dnx) -cface1. rewrite -(fconnect_invariant krF nxFyr) -(fconnect_invariant krF xFzr). exact: krE. elim: pd pr eqFpdr => [|xd pd IHpd] [|xr pr] //=. case=> /esym/(rootP cfaceC) xrFxd /IHpd->; congr (_ :: _). by rewrite /kd; have [yr -> /= /fconnect_invariant->] := pfrrP xrFxd. 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)