proposition: Lemma coloring_dual (k : G -> color) : @coloring (dual G) k <-> graph_coloring k.
proof: Proof. split=> [[kE' kF'] | [kE kN]]. split=> x; rewrite /= eq_sym. by rewrite -{1}(finv_f edgeI x) [_ == _]kE'. by rewrite -{1}(finv_f nodeI x) [_ == _]kF'. split; move=> /= x; rewrite eq_sym. by rewrite -{1}(f_finv edgeI x) [_ == _]kE. by rewrite -{1}(f_finv nodeI x) [_ == _]kN. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)