proposition: Lemma insetP (r : grect) p : reflect (subpred (gtouch p) r) (inset r p).
proof: Proof. case: r p => x0 x1 y0 y1 [x y]; rewrite /= -andbA -!ler_subr_addr. apply/(iffP and4P)=> [[lbx ubx lby uby] | r1x]. by apply/subgrectE; rewrite !(addrA _ 1 1) !lez_addr1 -!ltr_subr_addr. rewrite !ltr_subr_addr; have r1dx z := r1x (Gpoint (x + z) (y + z)). have [] := (r1dx 1, r1dx (-1)); rewrite /= !ler_add2l !ltr_add2l. by do ![case/implyP/andP | case/andP=> ? ?]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)