proposition: Lemma Path_of_proof (G : relType) (x : G) (p : seq G) : path (--) x p -> pathp x (last x p) p.
proof: Proof. by rewrite /pathp eqxx andbT. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)