proposition: Lemma adj_lpath (x y : D) : plain D -> adjn x y -> exists p, [/\ path clink x p, last x p = y & {subset p <= [predU cnode x & cnode y]}].
proof: Proof. move => plainD /exists_inP [z Z1 Z2]; rewrite inE in Z1. rewrite inE cnodeC -[edge z](f_finv nodeI) -cnode1 in Z2. have [p [P1 P2 P3]] := cnode_lpath Z1; have [q [Q1 Q2 Q3]] := cnode_lpath Z2. exists (p ++ finv node (edge z) :: q); split. - by rewrite cat_path P1 P2 /= Q1 andbT -plain_eq' // finv_f ?clinkF. - by rewrite last_cat. - move => v. rewrite mem_cat !inE !app_predE => /or3P [/P3 ->//|/eqP->|/Q3 H]. + by rewrite !inE [cnode y _]cnodeC Z2. + rewrite !inE in H *. by rewrite [cnode y v](connect_trans _ H) // cnodeC. 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)