proposition: Lemma exists_adjbox : exists ab, [/\ ab_proper ab, exists s, forall e i, ab_mr_proper (s, ab e) e i & forall e, mr_adj e -> gr_proper (ab e)].
proof: Proof. have /fin_all_exists[is_arc arcP] e: exists is_arc : bool, mr_adj e <-> is_arc. by have [] := Rclassic (mr_adj e); [exists true | exists false]. pose arc := {e : Er | is_arc e}; pose v (a : arc) := sval a. pose a_adj a := meet (not_corner m0) (border m0 (mr (v a).1) (mr (v a).2)). have{a_adj}/fin_all_exists[/= ap apP] a: a_adj a by have /arcP[[]] := valP a. pose cl i := closure (m0 (mr i)). pose cl_a a (r : rect) i := meet r (cl i) -> i \in v a. pose has_ar0 a := exists2 ar0, forall i, cl_a a ar0 i & ar0 (ap a). have{has_ar0} /fin_all_exists2[ar0 ar0a ar0p] a: has_ar0 a. have [ar0 ar0p]: exists ar0 : rect, ar0 (ap a). by exists (sep_rect (ap a) (ap a)); apply: mem_sep_rect. have /fin_all_exists2[ar ar_a ar_p] i: exists2 ar, cl_a a ar i & ar (ap a). have [a_i | a'i] := boolP (i \in v a); first by exists ar0. have [//|no_ar] := Rclassic (exists2 ar, cl_a a ar i & ar (ap a)). have{no_ar} cl_i_e: cl i (ap a). move=> U openU /openU[ar ar_e Uar]. have [//|m0i'U] := Rclassic (meet (m0 (mr i)) U); case: no_ar. by exists ar => // -[z [ar_z /(_ U _ _)/m0i'U[]//]]; apply: Uar. pose J := [:: i; (v a).1; (v a).2]; have [[me meP] [apPa1 apPa2]] := apP a. have /fin_all_exists[k kP] j: exists k : 'I_2, j \in J -> m0 (me k) (mr j). case Jj: (j \in J); last by exists ord0. have [|k /ltP-ltk2 []] := meP (mr j); last by exists (Ordinal ltk2). by split; [have [] := mrP j | have:= Jj; rewrite !inE => /or3P[]/eqP->]. have{me meP kP} inj_k: {in J &, injective k}. move=> j1 j2 /kP-m0mj1 /kP-m0mj2 Dkj. by have [_] := mrP j1; apply; apply/(m0tr _ m0mj2)/m0sym; rewrite -Dkj. have [/arcP[_ lta] /idPn[]] := (valP a, max_card (mem [seq k j | j in J])). by rewrite card_ord card_in_image ?(card_uniqP _) //= !inE a'i neq_ltn lta. exists (\big[(@cap_rect R)/ar0]_(i | i \notin v a) ar i) => [i|]; last first. by elim/big_rec: _ => // j r _ r_a; apply/mem_cap_rect. rewrite -big_filter; set I := filter _ _ => -[z [ar_z cli_z]]. have [ari_z | ari'z] := Rclassic (ar i z); first by apply/ar_a; exists z. suffices: i \notin I by rewrite mem_enum negbK. elim: I ar_z => // j I IH; rewrite big_cons => /mem_cap_rect[clj_z /IH-a'i]. by rewrite inE; case: eqP ari'z => // ->. pose ar1 a b := sep_rect (ap a) (ap b). have ar1_inj a b: meet (ar1 a b) (ar1 b a) -> a = b. move/meet_sep_rect/(_ _ (ar0p a))=> ar0ab; apply/esym/eqP/andP. have a_clb i: cl i (ap b) -> i \in v a. by move=> cli_b; apply/ar0a; exists (ap b). have [/arcP[_ lta] /arcP[_ ltb]] := (valP a, valP b). have [_ [_ /a_clb/orP[/idPn[] | Df2]]] := apP b. rewrite neq_ltn orbC (leq_ltn_trans _ ltb) // /v. by have [_ [/a_clb/pred2P[]->] _ //] := apP b; apply: ltnW. by have [_ [/a_clb/orP[//|/idPn[]]]] := apP b; rewrite neq_ltn -(eqP Df2) ltb. pose ar a := \big[@cap_rect R/ar0 a]_b ar1 b a. have ar_p a: ar a (ap a). rewrite /ar; elim/big_rec: _ => // b r _ r_a. by apply/mem_cap_rect; split; first apply: mem_sep_rect. have ar_a a i: cl_a a (ar a) i. rewrite /ar; elim/big_rec: _ => // b r _ r_b [z [/mem_cap_rect[_ r_z] i_z]]. by apply/r_b; exists z. have ar1ar a b: subregion (ar a) (ar1 b a). rewrite /ar -big_filter; set B := filter _ _ => z. have: b \in B by rewrite mem_enum. elim: B => //= c B IH_B; rewrite inE big_cons => cBb /mem_cap_rect[]. by case/predU1P: cBb => [-> | Bb _ /(IH_B Bb)]. have{ar1_inj ar1ar} ar_inj a b: meet (ar a) (ar b) -> a = b. by case=> z [a_z b_z]; apply/ar1_inj; exists z; split; apply/ar1ar. have /fin_all_exists2[ab0 ab0ap ar_ab] a := approx_rect (ar_p a). pose r0 := Grect 1 0 1 0; have not_r0 p: ~~ r0 p by case: p => -[[]|]. pose s := \sum_a (ab0 a).1; pose s_ a := \sum_(b | b != a) (ab0 b).1. have Ds a: s = s_ a + (ab0 a).1 by rewrite addnC [s](bigD1 a). pose ab_ a := refine_srect (s_ a).+1 (ab0 a). exists (fun e => if insub e is Some e then (ab_ e).2 else r0). have {}ar_ab a z: ab_ a z -> ar a z by move/in_refine_srect/ar_ab. split=> [e f p | | e [adj_e lte]]; last 1 first. - have [a _ _|/negP[]] := insubP; last exact/arcP. have [p _ /insetW-ab0a_p] := ab0ap a. by rewrite gr_proper_refine; apply/gr_properP; exists p. - have [a _ <- /= a_p | _ /idPn[]//] := insubP. have [b _ <- /= b_p | _ /idPn[]//] := insubP. rewrite (ar_inj a b) //; exists (scale_point R s.+1 p); split; apply/ar_ab. by rewrite (Ds a) -addSn; apply/mem_approx_scale. by rewrite (Ds b) -addSn; apply/mem_approx_scale. exists s.+1 => e i; case: insubP => //= a _ Da _; rewrite /= (Ds a) -addSn. split=> [e_i | [z [/ar_ab-a_z m0i_z]]]; last first. by rewrite -Da; apply/ar_a; exists z; split; last exists z. have{e_i} cli_a: cl i (ap a). by have [_ []] := apP a; rewrite /v Da; case/pred2P: e_i => ->. have /(in_refine_srect 1)[p /rect_approx[r r_a p_r] a_p] := ab0ap a. have{r_a} /cli_a[|z [m0iz r_z]] := r_a; first by exists r. suffices /(in_refine_inset (s_ a)): inset_srect (refine_srect 1 (ab0 a)) z. by rewrite /(srect_region _ z) /= -iterSr addnS; exists z. apply: sub_mem_approx (p_r z r_z)=> q /gtouch_l; apply/insetP: q. by rewrite -refine_inset. 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)