proposition: Lemma pathp_cat x y p1 p2 : pathp x y (p1++p2) = (pathp x (last x p1) p1) && (pathp (last x p1) y p2).
proof: Proof. by rewrite {1}/pathp cat_path last_cat /pathp eqxx andbT /= -andbA. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)