proposition: Lemma irred_upath (p : Path x y) : irred p -> upath x y (val p).
proof: Proof. move => Ip. rewrite /upath irredE nodesE in Ip *. rewrite Ip /=. by case: p {Ip}. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)