proposition: Lemma cube_colorable : four_colorable cube -> four_colorable G.
proof: Proof. unlock cube => [[k [kE kF]]]; exists (k \o (tsI CTnf)); split=> x. apply: contraFF (kE (tsI CTnf (edge x))) => /eqcP/= ->. by rewrite edgeK -2!(eqcP (kF _)). by apply/eqcP/esym; rewrite /= -4!(eqcP (kF _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring)