proposition: Lemma gtouch_chop1 d p : gtouch (halfg d) p = all (gchop1^~ p) (traject gface d 4).
proof: Proof. case: p => x y; rewrite /= andbT /gchop1 /gchop !(halfg_face, halfg_edge). case: (halfg d) => x0 y0; rewrite !(oddg_face, oddg_edge) !ccw4 /=. rewrite !(addrA _ 1 1) !ltz_addr1. by case: oddgP; rewrite /= -andbA -?ler_subr_addr; do !bool_congr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)