diff --git a/theories/gridmap.v b/theories/gridmap.v
index 319e337..b7c0c34 100644
--- a/theories/gridmap.v
+++ b/theories/gridmap.v
@@ -318,9 +318,10 @@ move=> d; apply/imageP/flatten_mapP=> [[/= u G'u ->] | [c ltc /mapP[z ltz ->]]].
   apply/mapP; exists (if ~~ odd c then x else y).
     by rewrite /c mem_iota; case: oddgP.
   rewrite {}/c /bbd /bbp; congr ((p0 + _) *+ 2 + _); last by case: oddgP.
-  by case: oddgP G'u; rewrite bbE ?addr0 ?ubx ?uby /= ?andbT /h1 /w1;
-     do [ rewrite andbC -lez_addr1 subrK ltrW // subr_ge0 -eqn0Ngt => /eqP->
-        | have [/idPn||->] := ltrgtP _%:Z; rewrite ?addrK // -lerNgt lez_addr1].
+  case: oddgP G'u; rewrite bbE ?addr0 ?ubx ?uby /= ?andbT /h1 /w1;
+    do ?by rewrite andbC -lez_addr1 subrK ltrW // subr_ge0 -eqn0Ngt => /eqP->.
+  - by have [/idPn||->] := ltrgtP bbh%:Z; rewrite ?addrK // -lerNgt lez_addr1.
+  - by have [/idPn||->] := ltrgtP bbw%:Z; rewrite ?addrK // -lerNgt lez_addr1.
 rewrite -[bbd c z]gedge2; set ed := gedge (bbd c z).
 suffices /andP[Ged]: (ed \in gmgrid) && ~~ bb (halfg ed) by exists (Gmdart Ged).
 rewrite mem_iota /= -ltz_nat in ltz; rewrite !inE in ltc.