proposition: Lemma mring_edge m p : p \in mring m -> gedge p \notin mring m.
proof: Proof. by rewrite !in_mring !inE => /andP[_ /negPf->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)