proposition: Corollary sgraph_four_color (G : sgraph) : kplanar G -> exists k : G -> color, sgraph_coloring k.
proof: Proof. move => kpl. wlog no_iso : G kpl / no_isolated G; last first. { have [[D f emb_f planar_D]] := Wagner no_iso kpl. have loopless_D := emb_loopless emb_f. have [k col_k] := graph_four_color loopless_D planar_D. exact: coloring_of_embedding emb_f col_k. } move=> W; pose A := [set x : G | [exists y, x -- y]]. have no_iso : no_isolated (induced A). { move=> x'; have := valP x'; rewrite inE => /existsP [y xy]. suff yA : y \in A by exists (Sub y yA). by rewrite !inE; apply/existsP; exists (val x'); rewrite sgP. } have [|k col_k] := W _ _ no_iso. exact: kplanar_minor (induced_minor _) _. pose k' (x : G) := if boolP (x \in A) is AltTrue p then k (Sub x p) else Color0. exists k'. move=> x y xy. rewrite /k' !altT ?inE => [||? ?]. - by apply/existsP; exists y. - by apply/existsP; exists x; rewrite sgP. - exact: col_k. 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)