proposition: Lemma edge_clink (x y : G) : x -- y -> exists p, [/\ path clink (emb_inv x) p, last (emb_inv x) p = (emb_inv y) & {subset [set f z | z in p] <= [set x;y]}].
proof: Proof. rewrite -{1}[x]emb_invK -{1}[y]emb_invK -emb_edge //. move/adj_lpath => /(_ (emb_plain emb_f)) [p [P1 P2 P3]]. exists p; split => // v /imsetP [z /P3 Hz] -> {v}; move: Hz. by rewrite !inE !(emb_vertex emb_f) !f_iinv ![f _ == _]eq_sym. 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)