proposition: Lemma gchop_edge d p : gchop (gedge d) p = ~~ gchop d p.
proof: Proof. rewrite /gchop halfg_edge oddg_edge; case: (halfg d) p => x0 y0 [x y] /=. by case: oddgP; rewrite /= -!ltNge ?lez_addr1 // -ltz_addr1 addrK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)