proposition: Lemma pathp_concat x y z p q : pathp x y p -> pathp y z q -> pathp x z (p++q).
proof: Proof. move => /andP[A B] /andP [C D]. rewrite pathp_cat (eqP B) /pathp -andbA. exact/and4P. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)