proposition: Lemma cm_extend_adj : {cm | cm_proper cm & forall e, gr_proper (ab0 e) -> madj (cm e.1) (cm e.2)}.
proof: Proof. pose cm i := refine_matte (cm0 i); pose ab e := refine_rect (ab0 e). have: cm_proper cm. move=> i j /hasP[p /= cmj_p cmi_p]; apply/cm0P/hasP. by exists (halfg p); rewrite /= -in_refine_mdisk. have abP: ab_proper ab by move=> e f p; rewrite !in_refine_rect; apply/ab0P. have ab0_adj e: gr_proper (ab0 e) = gr_proper (ab e). by rewrite (gr_proper_refine 1). pose cm_apart cm := [pred e | gr_proper (ab e) & ~~ madj (cm e.1) (cm e.2)]. pose coarse_inset (b : grect) m := coarse_in b m /\ has (inset b) m. have (e) i (b := ab e) (m := cm i) : cm_apart cm e -> [/\ i \in e -> coarse_inset b m & has b m -> i \in e]. - rewrite /= -ab0_adj => /andP[/abcm0P-/(_ i)[b_m e_i] _]. split=> [/b_m|] /hasP[p]. rewrite -[p]halfg_double -in_refine_matte -/(cm i) -/m => m_2p. rewrite -in_refine_rect refine_inset -/(ab e) -/b => /insetW-b1_2p. by split; [apply: refine_matte_coarse | apply/hasP; exists (p *+ 2)]. rewrite in_refine_matte in_refine_rect => mi_p ab_p. by apply/e_i/hasP; exists (halfg p). elim: {cm}_.+1 {-2}cm (ltnSn #|cm_apart cm|) => // n IHn cm le_cm_n abcmP cmP. have [cm_meet | ] := boolP [forall e, ~~ cm_apart cm e]. exists cm => // e ab_e; have:= forallP cm_meet e. by rewrite /= -ab0_adj ab_e negbK. rewrite -negb_exists negbK => /existsP/sigW/=[e cm'e]. have [/abcmP-/all_and2[cme_ab ab_e] /ltn_eqF-e1'2] := (cm'e, valP e). have cm1ab: has (inset (ab e)) (cm e.1). by have [] //:= cme_ab e.1; rewrite !inE eqxx. have [cm2ref cm2ab]: coarse_in (ab e) (cm e.2) /\ has (ab e) (cm e.2). have [|cm2ref cm2ab]:= cme_ab e.2; first by rewrite !inE eqxx orbT. by split; last apply/(sub_has _ cm2ab)/insetW. have cm2'1: ~~ has (cm e.2) (cm e.1) by apply: contraFN e1'2 => /cmP->. have [cm2 [cm2cm ab_cm2] cm12] := extend_madj cm2ref cm2ab cm1ab cm2'1. pose xcm := [eta cm with e.2 |-> cm2]. have{cm12 e1'2} xcm_e: ~~ cm_apart xcm e. by rewrite /= eqxx -val_eqE e1'2 cm12 andbF. have has'cm2 i: i != e.2 -> ~~ has cm2 (cm i). move=> e2'i; apply/hasPn=> p. have [-> | e1'i] := eqVneq i e.1; first by apply/contraL=> /ab_cm2/andP[]. have ab'i: ~~ has (ab e) (cm i) by apply/(contra (ab_e i))/norP. have cm2'i: ~~ has (cm e.2) (cm i) by apply: contra e2'i => /cmP->. apply: contraL => /ab_cm2/andP[_]; apply/contraL=> cmi_p /=. by rewrite negb_or (hasPn ab'i) ?(hasPn cm2'i). have madj_cm2 i: i != e.2 -> madj (cm i) (cm e.2) -> madj (cm i) cm2. move=> e2'i /hasP[d cmi_d cm2ed]; apply/hasP; exists d => //. move: cmi_d cm2ed; rewrite !(inE, in_mring) => /andP[r2_d _] /andP[ri_ed _]. by rewrite cm2cm // (hasPn _ _ ri_ed) ?has'cm2. have{madj_cm2} xcm'cm': subpred (cm_apart xcm) (cm_apart cm). move=> f /= /andP[->]; apply/contra. have [-> | e2'f1] := altP eqP; last by case: eqP => // ->; apply: madj_cm2. have [-> | e2'f2] := altP eqP; first by rewrite madj_irrefl. by rewrite madj_sym (madj_sym cm2); apply: madj_cm2. have: cm_proper xcm. move=> i j /=; do 2!have [-> | /has'cm2/negP] := altP eqP; rewrite has_sym //. by clear 2; apply: cmP. apply: IHn => [|f i bf m xcm'f]. move: le_cm_n; rewrite ltnS (cardD1 e) inE [_ && _]cm'e. apply/leq_ltn_trans/subset_leq_card/subsetP=> f xcm'f. by rewrite inE /= [f \in _]xcm'cm' // (memPn _ _ xcm'f). have bf'e p: ab e p -> ~ bf p by move=> ? /(abP e)D; rewrite D ?xcm'f in xcm_e. have /xcm'cm'/(abcmP f i)/= := xcm'f; rewrite -/bf /m /=. case: eqP => // -> -[e2bf bf_f]; split=> [/e2bf[cm2ref_bf cm2_bf]|]; last first. by case/hasP=> p /ab_cm2/andP[_ /orP[/bf'e//|*]]; apply/bf_f/hasP; exists p. split=> [p q bf_p Dpq|]; last first. by have [p /cm2cm-cm2p bf_p] := hasP cm2_bf; apply/hasP; exists p. without loss suffices IHpq: p q bf_p Dpq / p \in cm2 -> q \in cm2. by apply/idP/idP=> /IHpq-> //; rewrite !in_refine_rect Dpq in bf_p *. by case/ab_cm2/andP=> _ /orP[/bf'e//|cm2p]; rewrite cm2cm // (cm2ref_bf p q). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph order ssralg ssrnum ssrint) fourcolor(hypermap geometry color coloring patch snip grid) fourcolor(matte)