proposition: Lemma upath_rconsE (G: diGraph) (x y : G) p : x != y -> upath x y p -> path (--) x (rcons (behead (belast x p)) y) /\ uniq (rcons (belast x p) y).
proof: Proof. rewrite /upath/pathp; elim/last_ind : p x y => [x y /negbTE-> //|p z ? x y ?]. rewrite !belast_rcons last_rcons /= -andbA => /and4P [H1 H2 H3 /eqP<-]. by rewrite H1 H2 H3. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)