proposition: Theorem four_color_hypermap G : planar_bridgeless G -> four_colorable G.
proof: Proof. move=> geoG; apply: cube_colorable. have{geoG} geoGQ: planar_bridgeless_plain_precubic (cube G). split; last exact/cubic_precubic/cubic_cube. split; last exact: plain_cube. by split; [rewrite planar_cube | rewrite bridgeless_cube]; apply: geoG. pose n := #|cube G|.+1; move: geoGQ (leqnn n); rewrite {1}/n. elim: {G}n (cube G) => // n IHn G geoG; rewrite ltnS leq_eqVlt. case/predU1P=> [Dn | /IHn]; [rewrite -{n}Dn in IHn | exact]. have [// | noncolG] := decide_colorable G. by have [] := @unavoidability the_reducibility G. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cube present) fourcolor(unavoidability reducibility)