fact: Definition cc_coloring cc (k : G -> color) := invariant edge k =i insertE cc /\ invariant face k =1 G.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)