proposition: Lemma pmap_le n1 n2 : n1 <= n2 -> forall m, submap (pmap n1 m) (pmap n2 m).
proof: Proof. by move/in_pmap_le=> n2n1 m z1 z2 [/n2n1-n2z1 /n2n1-n2z2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)