proposition: Lemma map_cover {z1 z2}: implies (m z1 z2) (cover m z1 /\ cover m z2).
proof: Proof. by split=> mz12; split; [apply/(map_transr mz12) | apply/(map_transl mz12)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)