proposition: Lemma mring_equad d : ~~ has (equad (gface d)) m -> (end0g d \in map end0g (mring m)) = false.
proof: Proof. move=> m'fd; apply/mapP => -[d1 m_d1 Dp]. rewrite in_mring inE (contraTF (hasPn m'fd _)) {m'fd}// in m_d1. rewrite !(inE, in_gchop_rect) /gchop !halfg_face !oddg_face /end0g. rewrite -{Dp}(canLR (addrK _) Dp) -addrA; case: (halfg d) => x y. by do 2!case: oddgP; rewrite /= !lter_add2 ?ger_addl ?ler_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)