proposition: Lemma coloring_inj h k : injective h -> coloring k -> coloring (h \o k).
proof: Proof. move=> injh [kE kF]; split=> x; rewrite /invariant. by move: (kE x); rewrite -(invariant_inj edge k injh). by move: (kF x); rewrite -(invariant_inj face k injh). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)