proposition: Lemma colorable_patch : four_colorable G <-> (exists2 et, ring_trace bGd et & ring_trace bGr (rot 1 (rev et))).
proof: Proof. split=> [[k [kE kF]] | [et [kd [kdE kdF] Tkd] [kr [krE krF] Tkr]]]. exists (trace (map k bG)). exists (k \o hd); last by rewrite -map_comp. have kdF xd: k (hd (face xd)) == k (hd xd). exact/eqP/esym/(fconnect_invariant kF)/patch_face_d'/fconnect1. split=> // xd /=; rewrite -{2}[xd]edgeK -(eqP (kdF _)) /= hdN. by move: (hd _) => y; rewrite -{1}[y]nodeK (eqcP (kF _)) [_ == _]kE. exists (k \o hr); last by rewrite -trace_rev -map_rev -DbGr -map_comp. split=> x /=; first by rewrite hrE [_ == _]kE. by apply/eqcP/esym/(fconnect_invariant kF); rewrite -patch_face_r fconnect1. pose c0 := head_color (map kd (rev bGd)) +c head_color (map kr bGr). pose kd' := addc c0 \o kd; have Ic0 := can_inj (addKc c0). have{kdE} kd'E: invariant edge kd' =1 pred0. by move=> x; rewrite -(kdE x); apply: invariant_inj. have{Ic0 kdF} kd'F: invariant face kd' =1 Gd. by move=> x; rewrite -(kdF x); apply: invariant_inj. have{Tkd Tkr} Tkd': rev (map kd' bGd) = map kr bGr. move: Tkr; rewrite Tkd -trace_rev -!map_rev [in X in _ -> X]map_comp /c0. case: (rev bGd) => [|xd bGd']; first by case: bGr => // xr []. case: bGr => [|xr bGr'] Ekdr; first by case: bGd' Ekdr. rewrite /= -untrace_trace -map_cons trace_addc addcC addKc. by rewrite -map_cons Ekdr map_cons untrace_trace. move: {kd c0}kd' kd'E kd'F Tkd' => kd kdE /(_ _)/eqcP/= kdF Tkdr. have eq_kdr xd xr: hd xd = hr xr -> kd xd = kr xr. move=> eq_xdr; have b_xd: xd \in bGd by rewrite -EbGdr eq_xdr codom_f. have b_xr: xr \in rev bGr by rewrite mem_rev -EbGrd -eq_xdr codom_f. rewrite -(nth_index xd b_xd) -(nth_index xr b_xr). rewrite -!index_mem in b_xd b_xr. rewrite -(nth_map xr Color0) -?(nth_map xd Color0) // map_rev -Tkdr revK. by rewrite -(index_map Ihd) -(index_map Ihr) map_rev DbGr revK eq_xdr. have kP x : {xr | x = hr xr} + {xd | xd \notin bGd & x = hd xd}. have [xrP | xrP'] := boolP (x \in codom hr); [left | right]. by exists (iinv xrP); rewrite f_iinv. have xdP: x \in codom hd by case/orP: (EhdUr x) => // /idPn[]. by exists (iinv xdP); rewrite -?EbGdr f_iinv. pose k x := match kP x with inl u => kr (sval u) | inr u => kd (s2val u) end. exists k; split=> x; rewrite /k /=. case: (kP x) => [[xr /= ->] | [xd b'xd /= ->]]; rewrite -(hrE, hdE) //. by case: (kP _) => [[_ /=/Ihr<-] | [_ _ /=/esym/eq_kdr->]]; apply: krE. by case: (kP _) => [[_ /=/eq_kdr<-] | [_ _ /=/Ihd<-]]; apply: kdE. apply/eqP/esym; case: (kP x) => [[xr /= ->] | [xd b'xd /= ->]]. case: (kP _) => [[yr /= Dy] | [yd _ /=/esym/eqP]]. by apply: (fconnect_invariant krF); rewrite patch_face_r -Dy fconnect1. by rewrite -[yd]nodeK hdFrF -(eqcP (krF _)) kdF => /eqP/eq_kdr. by rewrite -hdF // -kdF; case: (kP _) => [[_ /=/eq_kdr <-] | [_ _ /=/Ihd <-]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)