proposition: Lemma pathp_shorten x y p : pathp x y p -> exists p', [/\ pathp x y p', uniq (x::p') & {subset p' <= p}].
proof: Proof. case/andP. case/shortenP => p' *. by exists p'. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)