fact: Hypothesis fin_colorable : forall m, finite_simple_map m -> colorable_with nc m.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)