proposition: Lemma in_pmap_le n1 n2 : n1 <= n2 -> subregion (in_pmap n1) (in_pmap n2).
proof: Proof. by move=> le_n12 z [i]; exists i; first apply: leq_trans le_n12. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)