proposition: Theorem four_color_finite m : finite_simple_map m -> colorable_with 4 m.
proof: Proof. intros fin_m. pose proof (discretize.discretize_to_hypermap fin_m) as [G planarG colG]. exact (colG (combinatorial4ct.four_color_hypermap planarG)). Qed.
imports: fourcolor(real realplane)