proposition: Lemma pmring_simple : uniq (map end0g pmring).
proof: Proof. rewrite [map _ _]/= /end0g !halfg_face !oddg_face oddg_double. by rewrite (map_inj_uniq (addrI _) [:: _; _; _; _]). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)