proposition: Lemma embedqz_central : {subset s0c <= hc}.
proof: Proof. have hc_walk x q: let s := walkq (node x) q in x \in ac -> edge x \in ac -> x \in hc -> all (mem ac) s -> map h s == walkq (node (h x)) q -> all hc s. - elim: q x => //= _. + move=> x ax_c _ _ _ /andP[/eqP hnx _]. by rewrite andbT -(inj_eq faceI) hnx -embedqz_face 1?(fclosed1 acF) ?nodeK. + move=> q IHq x ac_x ac_ex /eqP hex /andP[ac_nx ac_q]. rewrite eqseq_cons => /andP[/eqP hnx h_q]. have ac_enx: edge (node x) \in ac by rewrite (fclosed1 acF) nodeK. have ac_ennx: edge (node (node x)) \in ac by rewrite (fclosed1 acF) nodeK. have hc_nx: node x \in hc. by rewrite inE hnx -{2}[x]nodeK embedqz_face ?faceK ?eqxx. have hc_ennx: edge (node (node x)) \in hc. rewrite inE e2c {1}(canRL nodeK (n3c (ac_bc ac_x))). rewrite embedqz_face // hex -(canRL nodeK (n3m _)). by rewrite (canRL edgeK (e2m _)) -embedqz_face // nodeK hnx. rewrite [_ == _]hc_nx /qstepL IHq //. by rewrite e2c (canRL nodeK (n3c (ac_bc ac_x))) -fclosed1. by rewrite -[h (edge _)]faceK -embedqz_face // nodeK hnx. + move=> q IHq x ac_x ac_ex /eqP hex /andP[ac_nx ac_q]. rewrite eqseq_cons => /andP[/eqP hnx h_q]. have ac_enx: edge (node x) \in ac by rewrite (fclosed1 acF) nodeK. have ac_ennx: edge (node (node x)) \in ac by rewrite (fclosed1 acF) nodeK. have hc_nx: node x \in hc. by rewrite inE hnx -{2}[x]nodeK embedqz_face ?faceK ?eqxx. by rewrite [_ == _]hc_nx /qstepR IHq ?e2c ?hcE // (eqP hc_nx) hnx. + move=> ql IHql qr IHqr x ac_x ac_ex /eqP hex /andP[ac_nx]. rewrite !all_cat eqseq_cons map_cat eqseq_cat ?size_map ?size_walkq //. case/andP=> ac_ql ac_qr /and3P[/eqP hnx h_ql h_qr]. have ac_enx: edge (node x) \in ac by rewrite (fclosed1 acF) nodeK. have ac_ennx: edge (node (node x)) \in ac by rewrite (fclosed1 acF) nodeK. have hc_nx: node x \in hc. by rewrite inE hnx -{2}[x]nodeK embedqz_face ?faceK ?eqxx. have hc_ennx: edge (node (node x)) \in hc. rewrite inE e2c {1}(canRL nodeK (n3c (ac_bc ac_x))). rewrite embedqz_face // hex -(canRL nodeK (n3m _)). by rewrite (canRL edgeK (e2m _)) -embedqz_face // nodeK hnx. rewrite [_ == _]hc_nx /= /qstepL /qstepR IHql // ?IHqr // ?e2c ?hcE //. * by rewrite (eqP hc_nx) hnx. * by rewrite (canRL nodeK (n3c (ac_bc ac_x))) -fclosed1. by rewrite -[h (edge _)]faceK -embedqz_face // nodeK hnx. - move=> q IHq x ac_x ac_ex /eqP hex /andP[ac_enLnx ac_q]. rewrite eqseq_cons => /andP[/eqP henLnx h_q]. have ac_fex: face (edge x) \in ac by rewrite -fclosed1. have ac_ffex: face (face (edge x)) \in ac by rewrite -fclosed1. have hc_enLnx: edge (node (qstepL (node x))) \in hc. rewrite inE e2c henLnx /qstepL !(canRL nodeK (n3m _)) !e2m. rewrite (canRL nodeK (n3c (ac_bc ac_x))) (canRL edgeK (e2c _)). by rewrite (n3c (ac_bc _ )) // !embedqz_face // hex. rewrite [_ == _]hc_enLnx {1}/qstepL IHq ?henLnx //. by rewrite e2c -[x]edgeK /qstepL (canRL edgeK (e2c _)) !(n3c (ac_bc _)). - move=> q IHq x ac_x ac_ex /eqP hex /andP[ac_Rnx ac_q]. rewrite eqseq_cons => /andP[/eqP hRnx h_q]. have ac_enx: edge (node x) \in ac by rewrite (fclosed1 acF) nodeK. have ac_enenx: edge (node (edge (node x))) \in ac. by rewrite (fclosed1 acF) nodeK. have hc_Rnx: qstepR (node x) \in hc. by rewrite inE hRnx /qstepR -!(canF_eq faceK) -!embedqz_face ?nodeK. by rewrite [_ == _]hc_Rnx {1}/qstepR IHq ?e2c ?hcE // (eqP hc_Rnx) hRnx. have hc_x0: x0c \in hc by rewrite inE Dhx0 Dhex0. have hc_ex0: edge x0c \in hc by rewrite hcE. have [qzR _ _ Dac] := qz_ok. have s0_ac: s0c \subset ac by rewrite -(eq_subset_r Dac) ring_fband. have{Dac} Ehs0: map h s0c == s0m. apply/eqP; pose n := size (flatqz qz). have [Dnc Dnm]: size s0c = n /\ size s0m = n by rewrite !size_walkqz. rewrite -(take_size s0c) -(take_size s0m) Dnc Dnm. elim: {-2}n (leqnn n) => [|i IHi] lt_i_n; first by rewrite !take0. rewrite (take_nth x0c) ?Dnc // map_rcons Dhs0 (IHi (ltnW _)) //. by rewrite -take_nth // Dnm. apply: subsetP; move: s0_ac Ehs0; rewrite /s0c /s0m !subset_all. case: qz qzR => [] []//= _ q01 []//= _ q10 _; rewrite hc_x0 !all_cat map_cat /=. rewrite hc_ex0 !(eqseq_cons, eqseq_cat); last by rewrite size_map !size_walkq. case/and4P=> ac_x0 ac_q01 ax_ex0 ac_q10 /and4P[/eqP<- h_q01 /eqP<- h_q10]. rewrite /qstepR !hc_walk // ?e2c // ?(eqP hc_x0) //. by rewrite /qstepR (eqP hc_x0) e2c e2m in h_q10. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)