proposition: Lemma cover_pmap n z : cover (pmap n m0) z <-> in_pmap n z.
proof: Proof. by split=> [[] // | n_z]; have [_ _ /(map_cover m0P)[m0z _]] := n_z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)