proposition: Lemma colorable_mirror : four_colorable (mirror G) -> four_colorable G.
proof: Proof. by case=> k /coloring_mirror; exists k. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)