proposition: Lemma pmap_plain n m : plain_map m -> plain_map (pmap n m).
proof: Proof. move=> mP; split=> z1 z2 [n_z1 _ /(map_sym mP)m_z21] //. by move=> z3 [_ n_z3 /(map_transl mP m_z21)m_z13]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)