proposition: Lemma mring_uniq m : uniq (mring m).
proof: Proof. exact: map_uniq (mring_simple m). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)