proposition: Lemma ehexF d : subpred (equad d) (ehex (gface d)).
proof: Proof. by move=> p; rewrite !(inE, in_gchop_rect) halfg_face andbAC => /andP[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)