proposition: Lemma pmring_cycle : cycle mrlink pmring.
proof: Proof. by rewrite /= /mrlink -!end0g_face gface4 !eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)