proposition: Lemma madj_sym : symmetric madj.
proof: Proof. apply/symmetric_from_pre=> m1 m2 /hasP[d m2d m1ed]. by apply/hasP; exists (gedge d); rewrite ?inE ?gedge2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)