proposition: Lemma map_transl {z1 z2}: implies (m z1 z2) (forall z, m z1 z <-> m z2 z).
proof: Proof. by split=> mz12 z; split; apply/(map_trans mP); first apply/mS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)