proposition: Lemma mem_pcat_edgeR x y z (yz : y -- z) (p : Path x y) u : (u \in pcat p (edgep yz)) = (u == z) || (u \in p).
proof: Proof. rewrite mem_pcat mem_edgep. case: (altP (u =P y)) => //= [->|]; by rewrite ?path_end 1?orbC. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)