proposition: Lemma adjn_color (D : hypermap) (k : D -> color) x y : graph_coloring k -> adjn x y -> k x != k y.
proof: Proof. case => inv_edge inv_node /exists_inP [z Z1 Z2]. have -> : k x = k z by apply: fconnect_invariant Z1. have -> : k y = k (edge z) by apply: fconnect_invariant Z2. move: (inv_edge z) => /= E. by rewrite eq_sym E. 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)