proposition: Lemma refine_mcorner m r q (p := halfg q): p \in m -> inset r p -> (0 < mcorner m p)%N -> let ext_m_r xm := {subset [preim halfg of m] <= xm} /\ {subset xm <= [preim halfg of predU r m]} in {xm | ext_m_r xm & mcorner xm q < mcorner m p}%N.
proof: Proof. move=> m_p r_p mp_gt0 ext_m_r; pose m_pc c := p + halfg (- c + oddg q) \in m. pose xmE xm c0 c := (q - c \notin xm) = ~~ [|| c == c0, m_pc c | q - c \in xm]. have ext_along d: {xm : matte | ext_m_r xm & forall c, xmE xm (oddg d) c}. pose xr := refine_rect r; pose xm := refine_matte m. have xrExmh: coarse_in xr xm by apply: refine_matte_coarse. have xr_xm: has xr xm. by apply/hasP; exists q; rewrite ?in_refine_matte ?in_refine_rect 1?insetW. have xr_qd: inset xr (q - oddg d). rewrite -in_refine_rect refine_inset in r_p; apply/(insetP r_p). by case: oddgP (q) => -[x y] /=; rewrite !lter_add2. have[xm1 xm1P xrm_xm1 xm1c1] := coarse_extends_in xrExmh xr_xm xr_qd. exists xm1 => [|c]. split=> p1 xm1p1; first by rewrite (in_extension xm1P) ?in_refine_matte. by rewrite !inE -in_refine_rect -in_refine_matte [_ || _]xrm_xm1. rewrite /xmE orbA orb_idl // => /predU1P[->|] //. by rewrite /m_pc -halfg_add -in_refine_matte => /in_extension->. have [oq0 | o_q] := eqVneq (oddg q) 0; last first. have [xm mr_xm Dxm] := ext_along (ccw (ccw (oddg q))); exists xm => {mr_xm}//. rewrite /mcorner !{}Dxm /m_pc; rewrite -[p]addr0 in m_p. by case: oddgP o_q; rewrite ?m_p //=; have [[->]|] := norP; rewrite ?addnS. have{mp_gt0} [d o_d /negPf-m'pd]: {d | oddg d != 0 & p - oddg d \notin m}. have:= mp_gt0; rewrite /mcorner. by do ![set d := (d in p - d); case m'd: (~~ _); [by exists d | clear d m'd]]. have [xm mr_xm Dxm] := ext_along d; exists xm => {mr_xm}//. rewrite /mcorner !inE !{}Dxm /m_pc oq0. by case: oddgP o_d m'pd => //= _ ->; do !have [[->]|] := norP; rewrite ?addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)