proposition: Lemma embedqz_rlinked : rlink_connected [predI ac & hc].
proof: Proof. have ccRfband x a: x \in fband a -> rlink_connected [predI fband a & hc] -> node x \in hc -> rlink_connected [predI fband (rcons a (node x)) & hc]. - move=> aFx ccFa hc_nx y z; rewrite !inE -!rot1_cons !fband_rot !fband_cons. have aFenx: edge (node x) \in [predI fband a & hc]. by rewrite inE /= (fclosed1 (fbandF a)) nodeK aFx hcE. case yFnx: (cface y (node x)) => [] => [_ | {yFnx}]. case zFnx: (cface z (node x)) => [] => [_ | {zFnx}]. by exists [::]; rewrite //= /rlink faceK (same_cface yFnx) cfaceC zFnx. case/(ccFa _ _ aFenx)=> p; rewrite edgeK=> nxRp aFp. exists (node x :: p); first by rewrite /= {1}/rlink faceK yFnx. rewrite /= fband_rot fband_cons connect0 hc_nx; apply: sub_all aFp => t /=. by rewrite fband_rot fband_cons andb_orl orbC => ->. case zFnx: (cface z (node x)) => [] => [|{zFnx}]. case/ccFa/(_ aFenx)=> p nfyRp aFp _; exists (rcons p (edge (node x))). by rewrite rcons_path nfyRp last_rcons /= /rlink e2c cfaceC zFnx. rewrite all_rcons /= fband_rot fband_cons andb_orl orbC [l in l || _]aFenx. apply: sub_all aFp => t /=; rewrite fband_rot fband_cons andb_orl => ->. exact: orbT. move/ccFa=> ccFay /ccFay[p nfyRp aFp]; exists p => //. apply: sub_all aFp => t /=; rewrite fband_rot fband_cons andb_orl => ->. exact: orbT. have ccRwalk x a q: let s := walkq (node x) q in x \in fband a -> edge x \in fband a -> all (mem ac) a -> rlink_connected [predI fband a & hc] -> all [predI ac & hc] s -> rlink_connected [predI fband (a ++ s) & hc]. - elim: q x a => /=; try by move=> *; rewrite cats0. + by move=> _ x a ? _ _ ?; rewrite andbT cats1 => /andP[_]; apply: ccRfband. + move=> _ ql IHql x a aFx aFex a_ac ccRa /andP[/andP[ac_nx hc_nx] ac_ql]. rewrite -cat_rcons /qstepL; apply: IHql => //; last exact: ccRfband. * by rewrite -rot1_cons fband_rot fband_cons cface1 nodeK connect0. * rewrite e2c -2!(nodeK (node (node _))) (n3c (ac_bc ac_nx)) nodeK. by rewrite -cats1 fband_cat -(fclosed1 (fbandF a)) aFex. by rewrite all_rcons /= ac_nx. + move=> _ qr IHqr x a aFx _ a_ac ccRa /andP[/andP[ac_nx hc_nx] ac_qr]. rewrite -cat_rcons /qstepR; apply: IHqr => //; last exact: ccRfband. * by rewrite -cats1 fband_cat (fclosed1 (fbandF a)) nodeK aFx. * by rewrite e2c -rot1_cons fband_rot fband_cons connect0. by rewrite all_rcons /= ac_nx. + move=> _ ql IHql qr IHqr x a aFx aFex a_ac ccRa. rewrite all_cat => /and3P[/andP[ac_nx hc_nx] ac_ql ac_qr]. rewrite -cat_rcons catA /qstepR; apply: IHqr => //. * by rewrite cat_rcons fband_cat (fclosed1 (fbandF a)) nodeK aFx. * by rewrite e2c cat_rcons fband_cat fband_cons connect0 orbT. * rewrite cat_rcons all_cat a_ac /= ac_nx /=. by move: ac_ql; rewrite all_predI => /andP[]. rewrite /qstepL; apply: IHql => //; last exact: ccRfband. * by rewrite -rot1_cons fband_rot fband_cons cface1 nodeK connect0. * rewrite e2c -2!(nodeK (node (node _))) (n3c (ac_bc ac_nx)) nodeK. by rewrite -(fclosed1 (fbandF _)) -cats1 fband_cat aFex. by rewrite all_rcons /= ac_nx. + move=> _ qll IHq x a _ aFex a_ac ccRa /andP[/andP[ac_neLnx hc_neLnx] ac_q]. have ac_fex: face (edge x) \in ac. have [y /(allP a_ac)/=ac_y exFy] := hasP aFex. by rewrite -fclosed1 // (closed_connect acF exFy). have ac_ffex: face (face (edge x)) \in ac by rewrite -fclosed1. have Dffex: node (qstepL (node x)) = face (face (edge x)). rewrite /qstepL -{1}[x]edgeK (n3c (ac_bc ac_fex)). by rewrite (canRL edgeK (e2c _)) (n3c (ac_bc _)). rewrite -cat_rcons {2}/qstepL; apply: IHq => //. * by rewrite -rot1_cons fband_rot fband_cons connect0. * by rewrite e2c Dffex -cats1 fband_cat -!(fclosed1 (fbandF a)) /= aFex. * by rewrite all_rcons /= ac_neLnx. rewrite Dffex (canRL edgeK (e2c _)) in hc_neLnx *; apply: ccRfband => //. by rewrite -!(fclosed1 (fbandF a)). move=> _ qrr IHq x a aFx _ a_ac ccRa /andP[/andP[ac_Rnx hc_Rnx] ac_q]. have ac_enx: edge (node x) \in ac. have [y /(allP a_ac)/=ac_y xFy] := hasP aFx. by rewrite (fclosed1 acF) nodeK (closed_connect acF xFy). rewrite -cat_rcons {2}/qstepR; apply: IHq => //. * by rewrite 2!(fclosed1 (fbandF _)) /qstepR !nodeK -cats1 fband_cat aFx. * by rewrite e2c -rot1_cons fband_rot fband_cons connect0. * by rewrite all_rcons /= ac_Rnx. rewrite /qstepR; apply: ccRfband => //. by rewrite (fclosed1 (fbandF a)) nodeK. have [qzR _ _ Dac] := qz_ok. have: all [predI ac & hc] s0c. apply/allP=> y s0c_y /=; rewrite embedqz_central //. by rewrite -Dac (subsetP (ring_fband _)). move: qzR Dac; rewrite /s0c; case: qz => q0 q1 /=; rewrite all_cat /=. case: q0 => //= [_ q01]; case: q1 => //= [_ q10] _ Dac. case/and3P=> /andP[/andP[ac_x0 hc_x0] ac_q01] /andP[ac_ex0 hc_ex0] ac_q10. pose a := [:: x0c; edge x0c] ++ walkq (qstepR x0c) q01. pose a2 := a ++ walkq (qstepR (edge x0c)) q10. have ccRa2: rlink_connected [predI fband a2 & hc]. apply: (ccRwalk); rewrite // ?e2c //. - by rewrite fband_cons connect0. - by rewrite !fband_cons connect0 orbT. - by move: ac_q01; rewrite /= ac_x0 ac_ex0 all_predI => /andP[]. apply: (ccRwalk); rewrite // ?e2c //= ?fband_cons ?connect0 ?orbT //. by rewrite ac_x0 ac_ex0. rewrite -cat1s cats1 -{2}[x0c]faceK e2c; apply: ccRfband => //. - by rewrite fband_cons cfaceC fconnect1. - move=> x y; rewrite !inE !fband_cons !orbF => /andP[xFx0 _] /andP[yFx0 _]. by exists [::]; rewrite //= /rlink faceK (same_cface xFx0) cfaceC yFx0. by rewrite -{1}[x0c]e2c edgeK. have {}Dac: ac =i fband a2. by move=> x; rewrite -Dac !(fband_cons, fband_cat); do !bool_congr. move=> x y; rewrite !(Dac, inE) => a2Fx a2Fy. have [p nfxRp a2_p] := ccRa2 _ _ a2Fx a2Fy. by exists p => //; apply: sub_all a2_p => z; rewrite inE /= Dac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)