proposition: Lemma connected_matte (U : region) (m : smatte) : open U -> connected U -> subregion m U -> subregion U (smatte_interpolated m U).
proof: Proof. move=> Uopen Uconnected Um. set U1 := smatte_interpolated m U; pose U2 z := U z /\ ~ U1 z. have U12_U: subregion U (union U1 U2). by move=> z; case: (Rclassic (U1 z)); [left | right]. have U1_U: meet U1 U. suffices [z m_z]: {p | m p} by exists z; split; [exists m; split | apply/Um]. case: (m) => s [[|p] //=]. by exists (scale_point R s p); apply/mem_approx_scale/mem_head. have U1open: open U1. move=> z [m1 m1z]; pose inrU b z := inset_srect b z /\ subregion b U. pose s := m1.1; without loss m1_Uz: m1 @s m1z / exists2 b, inrU b z & b.1 = s. have{m1z} [m1z m1m Um1] := m1z; have /Uopen[r r_z Ur] := Um1 z m1z. have [b1 b1z r_b1] := approx_rect r_z => /(_ (refine_smatte b1.1 m1)). apply; first exact/refine_smatte_interpolant. exists (refine_srect s b1); last exact: addnC. by split=> [|t /in_refine_srect/r_b1/Ur//]; apply/in_refine_inset. have [n]: exists n, mem_approx s [pred p in m1.2 | mcorner m1.2 p < n] z. by have [[p]] := m1z; exists (mcorner m1.2 p).+1, p; last apply/andP. elim: n => [|n IHn] in m1 s m1_Uz m1z * => -[p Dp /andP[m1p m1n_p]] //. have{m1_Uz m1z} [[b [b_z Ub] Db1] [m1z m1m Um1]] := (m1_Uz, m1z). have [p_inner | p_corner] := posnP (mcorner m1.2 p). have{m1n_p Dp} [r r_z p_r] := rect_approx Dp; exists r => // t /p_r-r_t. by exists m1; split; first apply/(sub_mem_approx _ r_t)/mcorner0. have b_p: inset b.2 p. by case: b_z => q; rewrite /= Db1 => /(approx_point_inj Dp)<-. have [p2 Dp2] := approx_point_exists s.+1 z. have Ep2: halfg p2 = p by apply/(approx_point_inj _ Dp)/approx_halfg. have [|||m2 []] := @refine_mcorner m1.2 b.2 p2; rewrite Ep2 //. move=> m2m1 bm1m2 ltm; have m2p2: p2 \in m2 by rewrite m2m1 // inE Ep2. apply: (IHn (s.+1, m2)); last by exists p2; rewrite //= m2p2 (leq_trans ltm). exists (refine_srect 1 b); last by rewrite /= Db1. by split=> [|t bt]; [apply/in_refine_inset | apply/Ub/(in_refine_srect 1)]. split=> [|t /m1m/(in_refine_smatte 1) | t]; first by exists p2. by apply: sub_mem_approx t => q; rewrite /= in_refine_matte => /m2m1. case=> q2 /approx_halfg-Dq /bm1m2; rewrite !inE; set q := halfg q2 in Dq *. by case/orP=> [b_q | m1q]; [apply/Ub | apply/Um1]; exists q; rewrite // Db1. suffices{U1open} U2open: open U2. move=> z Uz; have /U12_U[// | U2z] := Uz. by have [] := Uconnected U1 U2 => // [|t [U1t [_ []]//]]; exists z; split. move=> z [/Uopen[r /approx_rect[b b_z r_b] Ur] U1'z]. suffices b'U1: ~ meet b U1. have [p /rect_approx[rp rp_z p_rp] b_p] := b_z; exists rp => // t /p_rp-p_t. have b_t: b t by apply: sub_mem_approx t p_t => q /gtouch_l/(insetP b_p). by split=> [|U1t]; [apply/Ur/r_b | have [] := b'U1; exists t]. case=> t [b_t [m1]]; move: r_b b_z b_t. without loss: b m1 / b.1 = m1.1 /\ coarse_in b.2 m1.2. pose b2 := refine_srect m1.1.+1 b; pose m2 := refine_smatte b.1.+1 m1. move=> IH r_b b_z b_t /(refine_smatte_interpolant b.1.+1). apply: (IH b2); last 1 [exact/in_refine_inset | exact/in_refine_srect]. by split; [rewrite /= addnC addnS | apply/refine_matte_coarse]. by move=> v /in_refine_srect/r_b. case: b => _ b /= [-> b_ref] r_b [p /= Dp b_p] [q /= Dq b_q] [m1t m1m Um1]. have{q Dq b_q m1t} b_m1: has b m1.2. by apply/hasP; exists q => //; have [_ /(approx_point_inj Dq)<-] := m1t. have [m2 m2m1 bm1m2 m2p] := coarse_extends_in b_ref b_m1 b_p. case: U1'z; exists (m1.1, m2); split=> [|u /m1m|u [q Dq]]; first by exists p. exact/sub_mem_approx/in_extension. by case/bm1m2/orP=> [b1q | m1q]; [apply/Ur/r_b | apply/Um1]; exists q. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph bigop ssralg ssrnum ssrint) mathcomp(div intdiv) fourcolor(hypermap geometry coloring grid matte gridmap) fourcolor(real realplane realprop approx)