proposition: Corollary graph_four_color (D : hypermap) : loopless D -> planar D -> graph_four_colorable D.
proof: Proof. rewrite -four_colorable_dual -planar_dual -bridgeless_dual => ? ?. exact: four_color_hypermap. 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)