proposition: Lemma pcat_subset (A : pred D) : p \subset A -> q \subset A -> pcat p q \subset A.
proof: Proof. move => /subsetP Hp /subsetP Hq. apply/subsetP => u. rewrite !mem_pcat. case/orP; [exact: Hp|exact: Hq]. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)