fact: Definition in_pmap n : region := fun z => exists2 i, i < n & m0 z 'z_i.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)