proposition: Lemma emb_path_f (x y : D) (p : Path (f x) (f y)) : exists q, [/\ path clink x q, last x q = y & {in q, forall z, f z \in p}].
proof: Proof. have [q [Q1 /emb_vertexP Q2 Q3]] := emb_path p. have Nx: cnode x (emb_inv (f x)) by rewrite (emb_vertex emb_f) emb_invK. have [q1 [Q11 Q12 Q13]] := cnode_lpath Nx. have [q2 [Q21 Q22 Q23]] := cnode_lpath Q2. exists (q1 ++ q ++ q2); rewrite !cat_path !last_cat Q11 Q12 Q1 Q21 Q22. split => // z; rewrite !mem_cat => /or3P[/Q13||/Q23]; try exact: Q3. - by move/emb_vertexP<-. - move/emb_vertexP<-. by rewrite (emb_vertexP _ _ Q2). Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)