proposition: Lemma has_cutout : gm_cutout Ir.
proof: Proof. have planGm := gmdart_planar; set E := Ir : pred Ir. elim: {E}_.+1 {-2}E (ltnSn #|E|) => // n IHn E leEn. have [j /= Ej | /(_ _)/=noE] := pickP [mem E]; last first. by exists gmdart_map id (rev \o gmring) => // i; rewrite ?noE ?map_id ?revK. rewrite ltnS (cardD1 j) Ej in leEn. have{IHn} [G h r planG Ih hE hF hN Dr cycNr] := IHn _ leEn. pose mj := [preim h of diskN (gmring j)]. have h_r i x: (h x \in gmring i) = (x \in rev (r i)). by rewrite -Dr !mem_rev mem_map. have cycRrj: scycle rlink (rev (r j)). have /andP[] := gmring_cycle j; rewrite -Dr -map_rev simple_map //. move=> cycRrj UFrj; have Urj := simple_uniq UFrj. rewrite /scycle cycle_from_next // => x /(map_f h)/(next_cycle cycRrj). by rewrite next_map // /rlink -hE hF. have r'mj i x: i != j -> x \in mj -> x \notin r i. move=> j'i mj_x; apply: contraL (disjoint_gmdisk j'i) => ri_x. by apply/existsP; exists (h x); rewrite /= diskN_E !inE h_r mem_rev ri_x. have mj_hN: {in mj, {morph h : x / node x}}. by move=> x mj_x; apply/hN/forall_inP=> i /andP[/r'mj->]. have mjN: fclosed node mj. apply/(intro_closed cnodeC)=> x _ /eqP<- mj_x; rewrite inE /= mj_hN //. by rewrite -(fclosed1 (diskN_node _)). have h_mj: {subset diskN (rev (r j)) <= mj}. move=> _ /hasP[z rj_z /connectP[s xDs ->]]; set x := finv node z in xDs *. have{rj_z} mj_x: x \in mj. by rewrite (fclosed1 mjN) (f_finv nodeI) !inE diskN_E !inE h_r rj_z. elim: s => //= y s IHs in {z} (x) mj_x xDs *. case/andP: xDs => /andP[/= rj'x xCy]; apply: {s}IHs; rewrite (fclosed1 mjN). case/clinkP: xCy => <- //; rewrite !inE diskN_E; apply/orP; right=> /=. rewrite (fclosed1 (diskE_edge gmdart_planar (gmring_cycle j))) -hE faceK. by rewrite !inE (h_r j) rj'x. have patch_j := snip_patch planG cycRrj; set Gj := snip_rem _ _ in patch_j. set hj : Gj -> G := snipr in patch_j. have [_ Ihj _ cycNrj _ _ _ _ _ hjN] := patch_j. pose rj i := preim_seq hj (rev (rev (r i))); have Drj i: map hj (rj i) = r i. rewrite map_preim revK // => x; rewrite codom_snipr !inE mem_rev. by apply: contraL => /andP[rj'x /h_mj/(r'mj i)-/implyP]; case: eqP => [->|]. have hjF x y: cface (hj x) (hj y) = cface x y by rewrite (patch_face_r patch_j). have h_rj i x: (hj x \in r i) = (x \in rj i) by rewrite -(mem_map Ihj) Drj. exists Gj (h \o hj) rj; first 1 [exact: planar_snipr | exact: inj_comp]. - by move=> x; rewrite /= hE. - by move=> x y; rewrite [LHS]hF hjF. - move=> x /forall_inP/=r'x; rewrite [y in h y]hjN ?(inE, r'x) //. by apply/hN/forall_inP=> i /andP[_ /r'x]; rewrite h_rj. - by move=> i; rewrite map_comp Drj Dr. move=> i Ei; have [-> // | j'i] := eqVneq i j. have [|cycNri Uri] := andP (cycNr i _); first exact/andP. have Urji: uniq (rj i) by rewrite -(map_inj_uniq Ihj) Drj. rewrite /ucycle cycle_from_next // => x /(map_f hj); rewrite Drj => r_x. have:= next_cycle cycNri r_x; rewrite -Drj next_map //= -hjN // !inE -h_rj. by apply: contraL r_x => rj_x; rewrite r'mj ?h_mj // diskN_E !inE mem_rev rj_x. 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)