proposition: Lemma eq_pmap_le {n1 n2 k k'} : n1 <= n2 -> implies (eq_pmap n2 k k') (eq_pmap n1 k k').
proof: Proof. by move/in_pmap_le=> n2_n1; split=> Ekk' z1 z2 /n2_n1-n2z1 /n2_n1; apply: Ekk'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)