proposition: Lemma in_gchop_rect d : gchop_rect d =1 predI r (gchop d).
proof: Proof. rewrite /gchop_rect /gchop; case: r (halfg d) => x0 x2 y0 y2 [x1 y1] [x y] /=. case: oddgP; rewrite /= (leUx, ltxI) ?ltz_addr1 -!andbA; 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)