proposition: Lemma upath_cons x y z p : upath x y (z::p) = [&& x -- z, x \notin (z::p) & upath z y p].
proof: Proof. rewrite /upath pathp_cons [z::p]lock /= -lock. case: (x -- z) => //. by case (uniq _). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)