fact: Definition sgraph_coloring (G : sgraph) (C : finType) (k : G -> C) := forall x y : G, x -- y -> k x != k y.
imports: HB(structures) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(sgraph connectivity minor excluded) fourcolor(hypermap geometry walkup color coloring combinatorial4ct) GraphTheory(set_tac) GraphTheory(hmap_ops smerge embedding arc K4plane)