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