proposition: Lemma irred_catE : irred (pcat p q) -> [/\ irred p, irred q & forall k, k \in p -> k \in q -> k = y].
proof: Proof. rewrite irred_cat. case/and3P => [? ? A]. split => // k K1 K2. apply/eqP. move/eqP/setP/(_ k) : A. by rewrite !inE K1 K2. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)