proposition: Lemma eqm_colorable : four_colorable G -> four_colorable G'.
proof: Proof. case: G eqG => [d e n f GeK] [e' n' f' G'eK De _ Df] [k [kE kF]]; exists k. by split=> x; rewrite /= -?De -?Df; [apply: kE | apply: kF]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)