proposition: Lemma path_end : y \in p.
proof: Proof. by rewrite mem_path nodesE -[in X in X \in _](path_last p) mem_last. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)