proposition: Lemma extend_madj (m1 : matte) (r : grect) : coarse_in r m -> has r m -> has (inset r) m1 -> ~~ has m m1 -> let m2 := [predD predU r m & m1] in {xm : matte | {subset m <= xm} /\ {subset xm <= m2} & madj m1 xm}.
proof: Proof. rewrite (has_sym m) => rEmh r_m /hasP/sig2W[p m1_p r_p] /negP-m1'm m2. have{rEmh r_m r_p} [xm xmP sxmr xm_p] := coarse_extends_in rEmh r_m r_p. have{p m1_p xm_p} m1_xm: has m1 xm by apply/hasP; exists p. elim: {xm}xmP => {m1'm}// p xm0 xm xm0P IHxm xm0ep Dxm in sxmr m1_xm. have sxm0r: {subset xm0 <= predU r m}. by move=> q xm0q; rewrite sxmr // !inE Dxm inE xm0q orbT. have [m1_xm0 | m1'xm0] := boolP (has m1 xm0); first exact: IHxm. exists xm0; first do [split; first exact: in_extension]. by move=> q xm1q; rewrite inE (hasPn m1'xm0) //= sxm0r. apply/hasP; exists (gedge p); rewrite //= gedge2 in_mring inE. rewrite andbC (hasPn m1'xm0); last by move: xm0ep; rewrite in_mring => /andP[]. by have [q] := hasP m1_xm; rewrite Dxm => /predU1P[-> | /(hasPn m1'xm0)/negP]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)