fact: Record subcoloring k : Prop := SubColoring { subcoloring_plain :> plain_map k; subcoloring_adj z1 z2 : adjacent m0 z1 z2 -> ~ k z1 z2; subcoloring_size : at_most_regions nc k }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)