proposition: Lemma end0g_equad d : ~~ has (equad (gface d)) m -> m (end0g d) = false.
proof: Proof. move/hasPn/(_ _)/contraTF; apply; rewrite !(inE, in_gchop_rect) /gchop. rewrite !halfg_face !oddg_face /end0g; case: (halfg d) => x y. by case: oddgP; rewrite /= !lter_add2 /= ?ler_addl ?ger_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)