proposition: Lemma in_pmap_trans n z : in_pmap n z -> subregion (m0 z) (in_pmap n).
proof: Proof. by case=> i ltin m0zi t m0zt; exists i => //; apply/(map_transl m0P m0zt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)