proposition: Lemma eq_map_pmap n k : eq_pmap n k (pmap n k).
proof: Proof. by split=> [|[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)