proposition: Lemma in_pmapP n z : in_pmap n z -> exists2 i, i < n & pmap n m0 z 'z_i.
proof: Proof. move=> n_z; have [i lt_i_n m0zi] := n_z; suffices: in_pmap n 'z_i by exists i. exact: in_pmap_trans n_z _ m0zi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)