proposition: Lemma coloring_of_embedding (G : sgraph) (D : hypermap) (f : D -> G) (k : D -> color) : embedding f -> graph_coloring k -> exists k' : G -> color, sgraph_coloring k'.
proof: Proof. move => emb_f [inv_edge inv_node]. exists (k \o emb_inv emb_f). move => x y /=. set dx := emb_inv _ x; set dy := emb_inv _ y. rewrite -[x](_ : f dx = x) -1?[y](_ : f dy = y); try exact: f_iinv. rewrite -emb_edge //. exact: adjn_color. Qed.
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)