proposition: Lemma coloring_mirror (k : G -> color) : @coloring (mirror G) k -> coloring k.
proof: Proof. case=> kE' kF'; have kF x: k (face x) = k x. by apply/esym/eqP; rewrite -{1}(finv_f faceI x) [_ == _]kF'. split=> x //=; rewrite eq_sym -kF ?eqxx // -(kF (edge x)) -{1}[x]edgeK. exact: kE'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)