proposition: Lemma pmap_extensible n1 n2 k : n1 <= n2 -> extensible n2 k -> extensible n1 (pmap n1 k).
proof: Proof. move=> le_n12 ext_k n; have [k' k'P /(eq_pmap_le le_n12)Ekk'] := ext_k n. by exists k' => //; apply/(eq_pmap_trans _ Ekk')/eq_pmap_sym/eq_map_pmap. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)