proposition: Lemma preembedding_simple_path : preembedding -> fclosed face A -> forall x y, edge x \in A -> y \in A -> exists2 p, [/\ path rlink x p, cface (last x p) y & p != [::]] & simple p /\ all [predI A & edge_central] p.
proof: Proof. case=> _ _ hfA heA Af x y Aex Ay; set B := [predI A & edge_central]. have /pred0Pn[z /andP[/= exFz zcE]] := subsetP hfA _ Aex. have{hfA} /pred0Pn[t /andP[/= yFt tcE]] := subsetP hfA _ Ay. have Bz: B z by rewrite !inE -[_ \in _](closed_connect Af exFz) Aex. have Bt: B t by rewrite !inE -[_ \in _](closed_connect Af yFt) Ay. have{heA} [p nfzRp Bp] := heA _ _ Bz Bt; rewrite -/B in Bp. have{nfzRp} xRp: path rlink x (rcons p t). by move: nfzRp; rewrite headI /= {1}/rlink faceK -(same_cface exFz). have [q [xRq Uq] [Eq Eq0 /allP sqp]] := simplify_rlink xRp. exists q; split=> //; first by rewrite -Eq last_rcons cfaceC. by rewrite (sameP eqP nilP) -Eq0 headI. by apply/allP=> u /sqp; apply/allP; rewrite all_rcons Bt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)