proposition: Lemma gchop_rect_edge d : r (halfg (gedge d)) -> forall p, gchop_rect d p -> gchop_rect d (halfg d).
proof: Proof. rewrite halfg_edge => r_ed [x y]; rewrite !in_gchop_rect /= gchop_halfg. rewrite /gchop; case: r (halfg d) => [x0 x2 y0 y2] [x1 y1] /= in r_ed *. rewrite andbT -!andbA -!lez_addr1 => /and5P[lbx ubx lby uby]. by case: oddgP r_ed; rewrite /= ?addr0 -andbA -!lez_addr1 ?subrK; case/and4P=> lbx1 ubx1 lby1 uby1 d_xy; apply/and4P; split=> //; rewrite ?lez_addr1 ?(le_trans _ d_xy, le_lt_trans d_xy) -?lez_addr1 //; apply/ltW; rewrite -lez_addr1 // -ler_subr_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)