proposition: Lemma pcoloring_le n1 n2 k : n1 <= n2 -> pcoloring n2 k -> pcoloring n1 k.
proof: Proof. by move=> len12 [k_n2 n_k]; split=> // z1 z2 n1z12; apply/n_k/(pmap_le len12). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)