proposition: Lemma madj_irrefl : irreflexive madj.
proof: Proof. by move=> m; apply/hasPn=> d; rewrite !inE !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)