proposition: Lemma four_colorable_dual : four_colorable (dual G) <-> graph_four_colorable G.
proof: Proof. by split=> [] [k colk]; exists k; case (coloring_dual k); auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)