proposition: Lemma patch_face_r xr yr : cface xr yr = cface (hr xr) (hr yr).
proof: Proof. apply/idP/idP. case/connectP=> p xFp ->{yr}. elim: p xr xFp => //= _ p IHp xr /andP[/eqP <- /IHp]; apply: connect_trans. have [b_fxr | /hrF->] := boolP (face xr \in bGr); last exact: fconnect1. have [xd Dfxr Dxd] := bGrP b_fxr; rewrite -{}Dfxr -[xr]faceK hrE -{}Dxd. by rewrite -{1}[xd]edgeK hdN cface1 nodeK patch_face_d' // cfaceC fconnect1. set x := hr xr => /connectP[p xFp Lp]. pose cFdr := exists2 xd, _ = hd xd & exists2 yd, hd yd = hr _ & cface yd xd. have: if x \in codom hr then x = hr xr else cFdr x xr by rewrite codom_f. elim: p {xr}x (xr) xFp Lp => [|z p IHp] x xr /= => [_ | /andP[/eqP-Dz zFp]] Lp. by rewrite -Lp codom_f => /Ihr->. have [xrP Dx | b'xd [xd Dxd [yd Dyd ydFxd]]] := ifPn. rewrite cface1 (IHp z) {p IHp zFp Lp}// -{z}Dz. have [fxrP | ] := ifP. have [b_fxr | /hrF->] := boolP (face xr \in bGr); last by rewrite Dx. have [xd Dfxr Dxd] := bGrP b_fxr; rewrite -Dfxr Dx -[xr]faceK hrE -Dxd. rewrite -{1}[xd]edgeK hdN nodeK; congr (hd _). apply/esym/(scycle_cface cycEbGd); last exact: fconnect1. by rewrite -EbGdr Dfxr codom_f. by rewrite -EbGdr -[hd _]nodeK -hdN edgeK Dxd -hrE faceK -Dx. rewrite im_hr !inE=> /norP[/negbNE/imageP[xd _ Dfx]]. rewrite Dfx (mem_map Ihd) => b'xd; exists xd => //. exists (edge (node xd)); last by rewrite -{2}[xd]nodeK fconnect1. by apply/eqP; rewrite hdErN hdN -Dfx Dx -{1}[xr]faceK hrE edgeK. rewrite (IHp z) {p IHp zFp Lp}// -{z}Dz. rewrite !im_hr !inE Dxd codom_f (mem_map Ihd) /= in b'xd *. rewrite -hdF // codom_f (mem_map Ihd) /=. have [b_fxd | b'fxd] := ifPn. rewrite -Dyd [yd](scycle_cface cycEbGd _ b_fxd) -?cface1r //. by rewrite -EbGdr Dyd codom_f. by exists (face xd) => //; exists yd; last by rewrite -cface1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)