proposition: Lemma cnode_lpath (x y : D) : cnode x y -> exists p, [/\ path clink x p, last x p = y & {subset p <= cnode x}].
proof: Proof. rewrite -same_fconnect_finv // => /connectP [p pth_p lst_p]; exists p; split => //. by apply: sub_path pth_p; apply: subrelUl. by apply: closed_path_sub pth_p => //= z1 z2 /eqP<- ?; rewrite cnode1r f_finv. 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)