fact: Definition prefix_coloring n k := [/\ submap k (pmap n k), extensible n k & minimal n k].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)