proposition: Lemma mem_pcat u : (u \in pcat p q) = (u \in p) || (u \in q).
proof: Proof. rewrite mem_pcatT. case A: (u \in p) => //=. rewrite mem_path !nodesE inE (_ : u == y = false) //. apply: contraFF A => /eqP->. exact: path_end. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)