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