proposition: Lemma size_pmap n k : plain_map k -> at_most_regions nc k -> at_most_regions nc (pmap n k).
proof: Proof. set kn := pmap n k => kP [f f_k]. pose kfn i := intersect (k (f i)) (in_pmap n). suffices [g g_k]: exists g, forall i, i < nc -> subregion (kfn i) (kn (g i)). exists g => z [n_z _ /f_k[i /ltP-lt_i_nc kiz]]. by exists i; [apply/ltP | apply/g_k]. elim: nc => [|i [g g_k]]; first by exists f. have [[t [k_fi_t n_t]] | kfn'i] := Rclassic (nonempty (kfn i)). exists [eta g with i |-> t] => j /=; rewrite ltnS. by case: (ltngtP j) => [/g_k||->] // _ z [/(map_transl kP k_fi_t)]. exists g => j; rewrite ltnS leq_eqVlt => /predU1P[->|/g_k//] z kfn_iz. by case: kfn'i; exists z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)