proposition: Lemma mem_pcat_edgeL x y z (xy : x -- y) (p : Path y z) u : (u \in pcat (edgep xy) p) = (u == x) || (u \in p).
proof: Proof. rewrite mem_pcat mem_edgep. case: (altP (u =P y)) => //= ->. by rewrite path_begin. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)