proposition: Lemma pmap_sub n m : submap (pmap n m) m.
proof: Proof. by move=> z1 z2 []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)