proposition: Lemma upath_irred p (Up : upath x y p) : irred (Build_Path (upathW Up)).
proof: Proof. rewrite irredE nodesE. exact: upath_uniq Up. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)