proposition: Lemma exists_smatte : exists s cm, forall i, proper_smatte (s, cm i) i [pred e : Er | i \in e].
proof: Proof. pose E i := enum [pred e : Er | i \in e]. suffices /fin_all_exists[m mP] i: exists m, proper_smatte m i [mem E i]. pose s_ i := \sum_(j | j != i) (m j).1. exists (\sum_i (m i).1), (fun i => (refine_smatte (s_ i) (m i)).2) => i. rewrite (bigD1 i) //= addnC; apply/refine_smatte_proper. by have [m_i m_E] := mP i; split=> // e; rewrite -mem_enum => /m_E. have: all [pred e : Er | i \in e] (E i) by apply/allP=> e; rewrite mem_enum. have [[_ m0open m0connect] _] := fin_m0. elim: {E}(E i) => [_|e E IHe /= /andP[e_i /IHe{IHe}[m [m_i m_E]]]]. have [/m0open[r r_i m0i_r] _] := mrP i. have [[s b] [p p_i /insetW-b_p] r_b] := approx_rect r_i. exists (s, point_matte p); split=> // z p_z; apply/m0i_r/r_b. by apply: sub_mem_approx p_z => _ /predU1P[] // ->. have [ab_e | ab'e] := boolP (gr_proper (ab e).2); last first. by exists m; split=> // f /predU1P[-> /idPn | /m_E]. have [/(_ e_i)[z [e_z m0i_z]] _] := abP i ab_e. have [m1 [m1z m1m m0im1]] := connected_matte (m0open _) (m0connect _) m_i m0i_z. exists m1; split=> // f /predU1P[-> _ | _ /m_E[]// t []]; first by exists z. by exists t; split; first apply/m1m. 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)