proposition: Lemma cface_snipd : {mono snipd : u v / cface u v}.
proof: Proof. have homFd: {homo snipd : u v / cface u v}. move=> u _ /connectP[p uFp ->]. elim: p u uFp => //= _ p IHp u /andP[/eqP<- /IHp]; apply: {IHp}connect_trans. rewrite /= /snipd_face; case: ifP => ru; last exact: fconnect1. by rewrite cfaceC -cface1; apply (prev_cycle cycRr ru). have homFd' u v : ~~ fband snipd_ring u -> cface (snipd u) (snipd v) -> cface u v. - move=> b'u /connectP[p]; elim: p => [|y p IHp] /= in u b'u *. by move=> _ /inj_snipd->. case/andP=> /eqP Dy yFp Lp. have r'u: (val u \notin r). apply: contra b'u => ru; apply/hasP; exists u => //. by rewrite -(mem_map inj_snipd) map_snipd_ring. have dNy: y \in diskN. rewrite (fclosed1 diskN_node) diskN_E (fclosed1 diskE_edge) orbC. by rewrite -Dy faceK inE /= r'u (valP u). apply: connect_trans {IHp yFp Lp}(IHp (sub y _) _ yFp Lp). by rewrite connect1 //= -val_eqE /= /snipd_face (negPf r'u) Dy. apply/hasP => [[w b_w yFw]]; case/hasP: b'u; exists w => //. apply: connect_trans yFw. by rewrite connect1 //= -val_eqE /= /snipd_face (negPf r'u) Dy. move=> u v; apply/idP/idP; last exact: homFd. have [b_u | ] := boolP (u \in fband snipd_ring); last exact: homFd'. have [b_v uFv | ] := boolP (v \in fband snipd_ring); last first. by rewrite (cfaceC u) cfaceC; apply: homFd'. have [[u1 ru1 uFu1] [v1 rv1 vFv1]] := (hasP b_u, hasP b_v). have u1Fv1: cface (snipd u1) (snipd v1). by rewrite (connect_trans (connect_trans _ uFv)) ?homFd ?(cfaceC u1). rewrite (same_cface uFu1) (same_connect_r cfaceC vFv1) eq_connect0 //. by apply/inj_snipd/(scycle_cface scycRr); rewrite // -map_snipd_ring map_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)