proposition: Lemma irred_catI : (forall k : D, k \in p -> k \in q -> k = y) -> irred p -> irred q -> irred (pcat p q).
proof: Proof. move => H Ip Iq. rewrite irred_cat Ip Iq /=. apply/eqP/setP => k. rewrite !inE. apply/andP/eqP => [[]|->]. exact: H. by rewrite path_begin path_end. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)