proposition: Lemma eq_pmap_sym n k k' : eq_pmap n k k' -> eq_pmap n k' k.
proof: Proof. by move=> Ekk'; split=> /Ekk'; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)