proposition: Lemma mem_edgep x y z (xy : x -- y) : z \in edgep xy = (z == x) || (z == y).
proof: Proof. by rewrite mem_path nodesE !inE. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)