proposition: Lemma pmring_def : pmring =i gborder pmdisk.
proof: Proof. move=> x; rewrite in_pmring !inE andb_idr // => /eqP<-. by rewrite eq_sym neq_halfg_edge. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)