proposition: Lemma pathp_cons x y z p : pathp x y (z :: p) = x -- z && pathp z y p.
proof: Proof. by rewrite -cat1s pathp_cat {1}/pathp /= eqxx !andbT. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)